let A be Subset of NAT ; :: thesis: ( ( for n, m being Element of NAT st n in A & m < n holds
m in A ) implies A is Cardinal )
assume A1: for n, m being Element of NAT st n in A & m < n holds
m in A ; :: thesis: A is Cardinal

per cases ( A = {} or ( A <> {} & ex m being Nat st
for n being Nat st n in A holds
n <= m ) or for m being Nat ex n being Nat st
( n in A & n > m ) ) ;

suppose A = {} ; :: thesis: A is Cardinal

hence A is Cardinal ; :: thesis: verum

end;

suppose that A2: A <> {} and
A3: ex m being Nat st
for n being Nat st n in A holds
n <= m ; :: thesis: A is Cardinal

defpred S₁[ set ] means $1 in A;
ex m being Element of NAT st S₁[m] by A2, SUBSET_1:10;
then A4: ex m being Nat st S₁[m] ;
consider M being Nat such that
A5: for n being Nat st S₁[n] holds
n <= M by A3;
consider m being Nat such that
A6: S₁[m] and
A7: for n being Nat st S₁[n] holds
n <= m from NAT_1:sch 6(A5, A4);
A = { l where l is Element of NAT : l < m + 1 }

proof

thus A c= { l where l is Element of NAT : l < m + 1 } :: according to XBOOLE_0:def 10 :: thesis: { l where l is Element of NAT : l < m + 1 } c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in { l where l is Element of NAT : l < m + 1 } )
assume A8: x in A ; :: thesis: x in { l where l is Element of NAT : l < m + 1 }
then reconsider l = x as Element of NAT ;
l <= m by A7, A8;
then l < m + 1 by NAT_1:13;
hence x in { l where l is Element of NAT : l < m + 1 } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Element of NAT : l < m + 1 } or x in A )
assume x in { l where l is Element of NAT : l < m + 1 } ; :: thesis: x in A
then consider l being Element of NAT such that
A9: x = l and
A10: l < m + 1 ;
l <= m by A10, NAT_1:13;
then ( l < m or l = m ) by XXREAL_0:1;
hence x in A by A1, A6, A9; :: thesis: verum

end;

hence A is Cardinal by AXIOMS:30; :: thesis: verum

end;

suppose A11: for m being Nat ex n being Nat st
( n in A & n > m ) ; :: thesis: A is Cardinal

NAT c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in A )
assume x in NAT ; :: thesis: x in A
then reconsider m = x as Element of NAT ;
ex n being Nat st
( n in A & n > m ) by A11;
hence x in A by A1; :: thesis: verum

end;

hence A is Cardinal by XBOOLE_0:def 10; :: thesis: verum

end;

end;