let M, N be Cardinal; :: thesis: ( M = N iff M,N are_equipotent )
thus ( M = N implies M,N are_equipotent ) ; :: thesis: ( M,N are_equipotent implies M = N )
consider A being Ordinal such that
A1: M = A and
A2: for C being Ordinal st C,A are_equipotent holds
A c= C by Def1;
consider B being Ordinal such that
A3: N = B and
A4: for C being Ordinal st C,B are_equipotent holds
B c= C by Def1;
assume M,N are_equipotent ; :: thesis: M = N
then ( B c= A & A c= B ) by A1, A2, A3, A4;
hence M = N by A1, A3, XBOOLE_0:def 10; :: thesis: verum