for n being Nat holds { k where k is Nat : k > n } is infinite