theorem Th12: :: CARD_1:13

for X being set holds not X, bool X are_equipotent