theorem :: XBOOLE_0:7

for X being set st X <> {} holds
ex x being object st x in X by Def1, Lm1;