let X be set ; :: thesis: ( ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) implies not X is finite )

A1: now

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

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume ex m being Element of NAT st
for n being Element of NAT st n >= m holds
not n in f .: k ; :: thesis: S₁[k + 1]
then consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
not n in f .: k ;
k + 1 = succ k by NAT_1:39
.= k \/ {k} by ORDINAL1:def 1 ;
then A4: f .: (k + 1) = (f .: k) \/ (Im f,k) by RELAT_1:153;

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 m' = f . k as Element of NAT ;
take max m,(m' + 1) ; :: thesis: for n being Element of NAT st n >= max m,(m' + 1) holds
not n in f .: (k + 1)
let n be Element of NAT ; :: thesis: ( n >= max m,(m' + 1) implies not n in f .: (k + 1) )
assume A6: n >= max m,(m' + 1) ; :: thesis: not n in f .: (k + 1)
then A7: not n in f .: k by A3, XXREAL_0:30;
n >= m' + 1 by A6, XXREAL_0:30;
then n <> m' by NAT_1:13;
then A8: not n in {m'} by TARSKI:def 1;
f .: (k + 1) = (f .: k) \/ {m'} by A4, A5, FUNCT_1:117;
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 Element of NAT st n >= m holds
not n in f .: (k + 1)
set m' = f . k;
let n be Element of NAT ; :: thesis: ( n >= m implies not n in f .: (k + 1) )
n <> f . k by A9;
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:117;
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:56;
take m ; :: thesis: for n being Element of NAT st n >= m holds
not n in f .: (k + 1)
let n be Element of 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:145
.= f .: {} by A12, XBOOLE_0:def 7
.= {} by RELAT_1:149 ;
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 Element of NAT st n >= 0 holds
not n in f .: 0
let n be Element of 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 by RELAT_1:149; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A14, A2); :: thesis: verum

end;

now

assume X is finite ; :: thesis: ex m being Element of NAT st
for n being Element of 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:146;
hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
not n in X by A1; :: thesis: verum

end;

hence ( ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) implies not X is finite ) ; :: thesis: verum