let m, n be Nat; :: thesis: ( m <= n implies <=6n+1 m c= <=6n+1 n )
assume A1: m <= n ; :: thesis: <=6n+1 m c= <=6n+1 n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <=6n+1 m or x in <=6n+1 n )
assume A2: x in <=6n+1 m ; :: thesis: x in <=6n+1 n
then reconsider x = x as Element of NAT ;
A3: x <= (6 * m) + 1 by A2, Th7;
6 * m <= 6 * n by A1, XREAL_1:64;
then (6 * m) + 1 <= (6 * n) + 1 by XREAL_1:6;
hence x in <=6n+1 n by A3, Th7, XXREAL_0:2; :: thesis: verum