theorem Th4: :: CARD_1:5

for X, Y being set holds
( X,Y are_equipotent iff card X = card Y )