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