let m, n be Nat; :: thesis: ( <=6n+1 m = <=6n+1 n implies m = n )
assume A1: <=6n+1 m = <=6n+1 n ; :: thesis: m = n
assume m <> n ; :: thesis: contradiction
then ( m < n or m > n ) by XXREAL_0:1;
hence contradiction by A1, Th10; :: thesis: verum