let A be Ordinal; :: thesis: card A c= A
( ex B being Ordinal st
( card A = B & ( for C being Ordinal st C,B are_equipotent holds
B c= C ) ) & A, card A are_equipotent ) by Def1, Def2;
hence card A c= A ; :: thesis: verum