let X, Y be set ; :: thesis: ( 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; :: thesis: ( card X = card Y implies X,Y are_equipotent )
assume card X = card Y ; :: thesis: X,Y are_equipotent
hence X,Y are_equipotent by A2, A1, WELLORD2:15; :: thesis: verum