theorem Th1: :: NUMBER13:1

for n being Nat holds
( not n < 3 or n = 0 or n = 1 or n = 2 )