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 )

hence
not for o being object holds o in X
; :: thesis: verum( 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;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