theorem th0b: :: FIELD_5:6
for n being Nat st n >= 3 holds
n +` n in exp (2,n)