theorem :: NAT_1:53

for n being natural Number holds
( n is zero or n = 1 or n > 1 )