let X be Subset of NAT; :: thesis: ( X is infinite implies ex N being increasing sequence of NAT st rng N c= X )
assume A1: X is infinite ; :: thesis: ex N being increasing sequence of NAT st rng N c= X
reconsider BX = bool X as non empty set by ZFMISC_1:def 1;
reconsider N0 = min* X as Element of NAT ;
reconsider Y0 = X as Element of BX by ZFMISC_1:def 1;
defpred S1[ object , object , set , object , set ] means ( $5 = $3 \ {$2} & $4 = min* $5 );
A2: for n being Nat
for x being Element of NAT
for y being Element of BX ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]
proof
let n be Nat; :: thesis: for x being Element of NAT
for y being Element of BX ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]
let x be Element of NAT ; :: thesis: for y being Element of BX ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]
let y be Element of BX; :: thesis: ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]
reconsider y1 = y \ {x} as Element of BX by XBOOLE_1:1;
set x1 = min* y1;
take min* y1 ; :: thesis: ex y1 being Element of BX st S1[n,x,y, min* y1,y1]
take y1 ; :: thesis: S1[n,x,y, min* y1,y1]
thus S1[n,x,y, min* y1,y1] ; :: thesis: verum
end;
consider N being sequence of NAT, Y being sequence of BX such that
A3: ( N . 0 = N0 & Y . 0 = Y0 & ( for n being Nat holds S1[n,N . n,Y . n,N . (n + 1),Y . (n + 1)] ) ) from RECDEF_2:sch 3(A2);
 defpred S2[ Nat] means ( N . $1 = min* (Y . $1) & N . $1 in Y . $1 & Y . $1 is infinite & Y . $1 c= NAT );
A4: S2[ 0 ] by A1, A3, NAT_1:def 1;
A5: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A6: S2[i] ; :: thesis: S2[i + 1]
A7: ( Y . (i + 1) = (Y . i) \ {(N . i)} & N . (i + 1) = min* (Y . (i + 1)) ) by A3;
A8: Y . (i + 1) is infinite
proof
assume Y . (i + 1) is finite ; :: thesis: contradiction
then (Y . (i + 1)) \/ {(N . i)} is finite ;
hence contradiction by A6, A7, XBOOLE_1:45, ZFMISC_1:31; :: thesis: verum
end;
Y . (i + 1) c= NAT by XBOOLE_1:1;
hence S2[i + 1] by A7, A8, NAT_1:def 1; :: thesis: verum
end;
A9: for i being Nat holds S2[i] from NAT_1:sch 2(A4, A5);
 A11: rng N c= X
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng N or y in X )
assume y in rng N ; :: thesis: y in X
then consider i being object such that
A10: ( i in NAT & N . i = y ) by FUNCT_2:11;
reconsider i = i as Nat by A10;
( N . i = min* (Y . i) & N . i in Y . i & Y . i is infinite & Y . i c= NAT ) by A9;
hence y in X by A10; :: thesis: verum
end;
for i being Nat holds N . i < N . (i + 1)
proof
let i be Nat; :: thesis: N . i < N . (i + 1)
A12: ( N . i = min* (Y . i) & N . i in Y . i & Y . i is infinite & Y . i c= NAT ) by A9;
( Y . (i + 1) = (Y . i) \ {(N . i)} & N . (i + 1) = min* (Y . (i + 1)) ) by A3;
then A13: N . (i + 1) in (Y . i) \ {(N . i)} by A9;
then ( N . (i + 1) in Y . i & not N . (i + 1) in {(N . i)} ) by XBOOLE_0:def 5;
then A14: N . (i + 1) <> N . i by TARSKI:def 1;
N . i <= N . (i + 1) by A12, A13, NAT_1:def 1;
hence N . i < N . (i + 1) by A14, XXREAL_0:1; :: thesis: verum
end;
then N is increasing ;
hence ex N being increasing sequence of NAT st rng N c= X by A11; :: thesis: verum