let M, N be Cardinal; :: thesis: ( M,N are_equipotent implies M = N )
A1: ex A being Ordinal st
( M = A & ( for C being Ordinal st C,A are_equipotent holds
A c= C ) ) by Def1;
ex B being Ordinal st
( N = B & ( for C being Ordinal st C,B are_equipotent holds
B c= C ) ) by Def1;
hence ( M,N are_equipotent implies M = N ) by A1; :: thesis: verum