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