let X, Y be set ; ( X,Y are_equipotent iff card X = card Y )
A1:
Y, card Y are_equipotent
by Def2;
A2:
X, card X are_equipotent
by Def2;
hence
( X,Y are_equipotent implies card X = card Y )
by Def2, WELLORD2:15; ( card X = card Y implies X,Y are_equipotent )
assume
card X = card Y
; X,Y are_equipotent
hence
X,Y are_equipotent
by A2, A1, WELLORD2:15; verum