let m, n be Nat; :: thesis: ( m < n implies Fermat m < Fermat n )
assume m < n ; :: thesis: Fermat m < Fermat n
then 2 |^ m < 2 |^ n by PEPIN:66;
then 2 |^ (2 |^ m) < 2 |^ (2 |^ n) by PEPIN:66;
hence Fermat m < Fermat n by XREAL_1:6; :: thesis: verum