let X, Y be set ; :: thesis: ( X,Y are_equipotent iff card X = card Y )
A1: ( X, card X are_equipotent & Y, card Y are_equipotent ) by Def5;
thus ( X,Y are_equipotent implies card X = card Y ) :: thesis: ( card X = card Y implies X,Y are_equipotent )

proof

assume X,Y are_equipotent ; :: thesis: card X = card Y
then card X,Y are_equipotent by A1, WELLORD2:22;
hence card X = card Y by Def5; :: thesis: verum

end;

assume card X = card Y ; :: thesis: X,Y are_equipotent
hence X,Y are_equipotent by A1, WELLORD2:22; :: thesis: verum