This is the so-called drinker paradox: there is someone in the pub such that, if he is drinking, everyone in the pub is drinking. Its proof essentially uses the law of excluded middle or double-negation elimination.

Do you need a formal proof? If so, which proof system you are using?