let X be set ; :: thesis: ( ( for m being Nat ex n being Nat st
( n >= m & n in X ) ) implies X is infinite )

A1: now :: thesis: for f being Function
for k being Nat holds S₁[k]

let f be Function; :: thesis: for k being Nat holds S₁[k]
defpred S₁[ Nat] means ex m being Nat st
for n being Nat st n >= m holds
not n in f .: $1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume ex m being Nat st
for n being Nat st n >= m holds
not n in f .: k ; :: thesis: S₁[k + 1]
then consider m being Nat such that
A3: for n being Nat st n >= m holds
not n in f .: k ;
Segm (k + 1) = (Segm k) \/ {k} by AFINSQ_1:2;
then A4: f .: (k + 1) = (f .: k) \/ (Im (f,k)) by RELAT_1:120;

per cases ( ( k in dom f & f . k in NAT ) or ( k in dom f & not f . k in NAT ) or not k in dom f ) ;

suppose A5: ( k in dom f & f . k in NAT ) ; :: thesis: S₁[k + 1]

then reconsider m9 = f . k as Element of NAT ;
set M = max (m,(m9 + 1));
reconsider M = max (m,(m9 + 1)) as Element of NAT by ORDINAL1:def 12;
take M ; :: thesis: for n being Nat st n >= M holds
not n in f .: (k + 1)
let n be Nat; :: thesis: ( n >= M implies not n in f .: (k + 1) )
assume A6: n >= M ; :: thesis: not n in f .: (k + 1)
then A7: not n in f .: k by A3, XXREAL_0:30;
n >= m9 + 1 by A6, XXREAL_0:30;
then n <> m9 by NAT_1:13;
then A8: not n in {m9} by TARSKI:def 1;
f .: (k + 1) = (f .: k) \/ {m9} by A4, A5, FUNCT_1:59;
hence not n in f .: (k + 1) by A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A9: ( k in dom f & not f . k in NAT ) ; :: thesis: S₁[k + 1]

take m ; :: thesis: for n being Nat st n >= m holds
not n in f .: (k + 1)
set m9 = f . k;
let n be Nat; :: thesis: ( n >= m implies not n in f .: (k + 1) )
n <> f . k by A9, ORDINAL1:def 12;
then A10: not n in {(f . k)} by TARSKI:def 1;
assume n >= m ; :: thesis: not n in f .: (k + 1)
then A11: not n in f .: k by A3;
f .: (k + 1) = (f .: k) \/ {(f . k)} by A4, A9, FUNCT_1:59;
hence not n in f .: (k + 1) by A11, A10, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not k in dom f ; :: thesis: S₁[k + 1]

then A12: dom f misses {k} by ZFMISC_1:50;
take m ; :: thesis: for n being Nat st n >= m holds
not n in f .: (k + 1)
let n be Nat; :: thesis: ( n >= m implies not n in f .: (k + 1) )
assume A13: n >= m ; :: thesis: not n in f .: (k + 1)
Im (f,k) = f .: ((dom f) /\ {k}) by RELAT_1:112
.= f .: {} by A12, XBOOLE_0:def 7
.= {} ;
hence not n in f .: (k + 1) by A3, A4, A13; :: thesis: verum

end;

end;

end;

A14: S₁[ 0 ]

proof

take 0 ; :: thesis: for n being Nat st n >= 0 holds
not n in f .: 0
let n be Nat; :: thesis: ( n >= 0 implies not n in f .: 0 )
assume n >= 0 ; :: thesis: not n in f .: 0
thus not n in f .: 0 ; :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A2); :: thesis: verum

end;

now :: thesis: ( X is finite implies ex m being Nat st
for n being Nat st n >= m holds
not n in X )

assume X is finite ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
not n in X
then consider f being Function such that
A15: rng f = X and
A16: dom f in omega by FINSET_1:def 1;
reconsider k = dom f as Element of NAT by A16;
f .: k = X by A15, RELAT_1:113;
hence ex m being Nat st
for n being Nat st n >= m holds
not n in X by A1; :: thesis: verum

end;

hence ( ( for m being Nat ex n being Nat st
( n >= m & n in X ) ) implies X is infinite ) ; :: thesis: verum