let n be Nat; :: thesis: { k where k is Nat : k > n } is infinite
set X = { k where k is Nat : k > n } ;
A1: { k where k is Nat : k > n } c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k > n } or x in NAT )
assume x in { k where k is Nat : k > n } ; :: thesis: x in NAT
then ex k being Nat st
( x = k & k > n ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

n + 1 > n + 0 by XREAL_1:8;
then A2: n + 1 in { k where k is Nat : k > n } ;
assume { k where k is Nat : k > n } is finite ; :: thesis: contradiction
then reconsider X = { k where k is Nat : k > n } as non empty finite Subset of NAT by A1, A2;
set m = max X;
max X in X by XXREAL_2:def 8;
then consider k being Nat such that
A3: max X = k and
A4: k > n ;
k + 1 > k + 0 by XREAL_1:8;
then k + 1 > n by A4, XXREAL_0:2;
then (max X) + 1 in X by A3;
then (max X) + 1 <= (max X) + 0 by XXREAL_2:def 8;
hence contradiction by XREAL_1:8; :: thesis: verum