let n be Nat; :: thesis: Fermat n > 2
set 2N = 2 |^ (2 |^ n);
2 |^ (2 |^ n) > 1 by Lm2;
then (2 |^ (2 |^ n)) + 1 > 1 + 1 by XREAL_1:6;
hence Fermat n > 2 ; :: thesis: verum