theorem :: NAT_1:23

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