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

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

set X = { k where k is Nat : k > n } ;

A1: { k where k is Nat : k > n } c= NAT

proof

n + 1 > n + 0
by XREAL_1:8;
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;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

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