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