let X be set ; :: thesis: not for o being object holds o in X

now :: thesis: ex u being object st
( u in bool X & not u in X )

assume for u being object st u in bool X holds
u in X ; :: thesis: contradiction
then bool X c= X ;
then B: card (bool X) c= card X by CARD_1:11;
card X in card (bool X) by CARD_1:14;
hence contradiction by B, CARD_1:3; :: thesis: verum

end;

hence not for o being object holds o in X ; :: thesis: verum