let M be set ; :: thesis: ( M is cardinal implies M is ordinal )
assume M is cardinal ; :: thesis: M is ordinal
then ex B being Ordinal st
( M = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) by Def1;
hence M is ordinal ; :: thesis: verum