for n being Nat st n >= 3 holds
n +` n in exp (2,n)