theorem :: NAT_1:25

for n being natural Number holds
( not n <= 1 or n = 0 or n = 1 )