theorem :: CARD_1:25

for X, Y being set st bool Y c= X holds
( card Y in card X & not Y,X are_equipotent )