theorem :: PRE_CIRC:23

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