let n be Nat; :: thesis: Fermat n > 1
Fermat n <> 1 by Th55;
then ( Fermat n > 1 or Fermat n < 1 ) by XXREAL_0:1;
hence Fermat n > 1 by NAT_1:14; :: thesis: verum