theorem Th22: :: NAT_1:22

for m, n being natural Number holds
( not m < n + 1 or m < n or m = n )