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