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