let n be Nat; :: thesis: ( n >= 3 implies n +` n in exp (2,n) )
assume AS: n >= 3 ; :: thesis: n +` n in exp (2,n)
n +` n = n + n by th0a;
then n +` n < 2 |^ n by AS, th0n;
then n +` n in 2 |^ n by th0k;
hence n +` n in exp (2,n) by th0e; :: thesis: verum