theorem Th16: :: NUMBER10:16

for m, n being non zero Nat st m <= n holds
LP<=6n+1 m <= LP<=6n+1 n