let n be Nat; :: thesis: not Fermat n is even
( (Fermat n) - 1 = (Fermat n) -' 1 & ((Fermat n) -' 1) mod 2 = 0 ) by Lm13, XREAL_0:def 2;
hence not Fermat n is even by NAT_2:21; :: thesis: verum