let n be Nat; :: thesis: (Fermat n) -' 1 > 0
Fermat n > 1 by Lm12;
then (Fermat n) - 1 > 1 - 1 by XREAL_1:9;
hence (Fermat n) -' 1 > 0 by XREAL_0:def 2; :: thesis: verum