let X be infinite Subset of NAT; :: thesis: for a being Nat ex b being Nat st
( b > a & b in X )
let a be Nat; :: thesis: ex b being Nat st
( b > a & b in X )
assume for b being Nat holds
( not b > a or not b in X ) ; :: thesis: contradiction
then P1: for b being Nat st b in X holds
b <= a ;
X c= (Seg a) \/ {0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (Seg a) \/ {0} )
assume A1: x in X ; :: thesis: x in (Seg a) \/ {0}
then reconsider xx = x as Nat ;
P2: xx <= a by P1, A1;
( 0 = xx or 0 + 1 <= xx ) by NAT_1:14;
then ( xx in {0} or xx in Seg a ) by P2, TARSKI:def 1;
hence x in (Seg a) \/ {0} by XBOOLE_0:def 3; :: thesis: verum

end;

hence contradiction ; :: thesis: verum