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
hence <=6n+1 m c= <=6n+1 n by Th9; :: according to XBOOLE_0:def 8 :: thesis: not <=6n+1 m = <=6n+1 n
6 * m < 6 * n by A1, XREAL_1:68;
then (6 * m) + 1 < (6 * n) + 1 by XREAL_1:8;
then not (6 * n) + 1 in <=6n+1 m by Th7;
hence not <=6n+1 m = <=6n+1 n ; :: thesis: verum