let m, n be Nat; :: thesis: ( m <= n implies Fermat m <= Fermat n )
assume m <= n ; :: thesis: Fermat m <= Fermat n
then ( m < n or m = n ) by XXREAL_0:1;
hence Fermat m <= Fermat n by Th30; :: thesis: verum