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: 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;

A3: 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
A4: 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 A5: 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 A6: ( k in dom f & f . k in NAT ) ; :: thesis: S₁[k + 1]

then reconsider m' = f . k as Element of NAT ;
A7: f .: (k + 1) = (f .: k) \/ {m'} by A5, A6, FUNCT_1:117;
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 n >= max m,(m' + 1) ; :: thesis: not n in f .: (k + 1)
then ( n >= m & n >= m' + 1 ) by XXREAL_0:30;
then ( n >= m & n <> m' ) by NAT_1:13;
then ( not n in f .: k & not n in {m'} ) by A4, TARSKI:def 1;
hence not n in f .: (k + 1) by A7, XBOOLE_0:def 3; :: thesis: verum

end;

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

set m' = f . k;
A9: f .: (k + 1) = (f .: k) \/ {(f . k)} by A5, A8, FUNCT_1:117;
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 n >= m ; :: thesis: not n in f .: (k + 1)
then ( n >= m & n <> f . k ) by A8;
then ( not n in f .: k & not n in {(f . k)} ) by A4, TARSKI:def 1;
hence not n in f .: (k + 1) by A9, XBOOLE_0:def 3; :: thesis: verum

end;

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

then A10: dom f misses {k} by ZFMISC_1:56;
A11: Im f,k = f .: ((dom f) /\ {k}) by RELAT_1:145
.= f .: {} by A10, XBOOLE_0:def 7
.= {} by RELAT_1:149 ;
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 n >= m ; :: thesis: not n in f .: (k + 1)
hence not n in f .: (k + 1) by A4, A5, A11; :: thesis: verum

end;

end;

end;

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

end;

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 )

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
A12: ( rng f = X & dom f in omega ) by FINSET_1:def 1;
reconsider k = dom f as Element of NAT by A12;
f .: k = X by A12, 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