theorem :: BOOLE:7

for x, X being set st x in X holds
not X is empty by XBOOLE_0:def 1;