let x be object ; :: thesis: ( x in omega implies x is cardinal )
assume that
A1: x in omega and
A2: for B being Ordinal st x = B holds
ex C being Ordinal st
( C,B are_equipotent & not B c= C ) ; :: according to CARD_1:def 1 :: thesis: contradiction
reconsider A = x as Ordinal by A1;
consider B being Ordinal such that
A3: B,A are_equipotent and
A4: not A c= B by A2;
B in A by A4, ORDINAL1:16;
then B in omega by A1, ORDINAL1:10;
then reconsider n = A, m = B as Nat by A1;
n,m are_equipotent by A3;
hence contradiction by A4, Lm2; :: thesis: verum