let m, n be non zero Nat; :: thesis: ( (6 * n) + 1 is prime & m < n implies LP<=6n+1 m < LP<=6n+1 n )
set A = <=6n+1 m;
set x = LP<=6n+1 m;
set y = LP<=6n+1 n;
assume that
A1: (6 * n) + 1 is prime and
A2: m < n ; :: thesis: LP<=6n+1 m < LP<=6n+1 n
A3: LP<=6n+1 m <= LP<=6n+1 n by A2, Th16;

now :: thesis: not LP<=6n+1 m = LP<=6n+1 n

assume A4: LP<=6n+1 m = LP<=6n+1 n ; :: thesis: contradiction
LP<=6n+1 m in (<=6n+1 m) /\ SetPrimes by XXREAL_2:def 8;
then A5: LP<=6n+1 m in <=6n+1 m by XBOOLE_0:def 4;
(6 * n) + 1 = LP<=6n+1 n by A1, Th32;
then 6 * n <= 6 * m by A4, A5, Th7, XREAL_1:6;
hence contradiction by A2, XREAL_1:68; :: thesis: verum

end;

hence LP<=6n+1 m < LP<=6n+1 n by A3, XXREAL_0:1; :: thesis: verum