theorem Th3: :: NUMBER13:3
for n being Nat holds
( not n < 5 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )