theorem :: CARD_2:2

for X being set holds
( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )