let m be non zero Nat; :: thesis: ( (6 * m) + 1 is prime implies (6 * m) + 1 = LP<=6n+1 m )
assume A1: (6 * m) + 1 is prime ; :: thesis: (6 * m) + 1 = LP<=6n+1 m
set x = (6 * m) + 1;
set A = <=6n+1 m;
A2: (6 * m) + 1 in <=6n+1 m ;
(6 * m) + 1 in SetPrimes by A1, NEWTON:def 6;
then A3: (6 * m) + 1 in (<=6n+1 m) /\ SetPrimes by A2, XBOOLE_0:def 4;
for a being ExtReal st a in (<=6n+1 m) /\ SetPrimes holds
a <= (6 * m) + 1

proof

let a be ExtReal; :: thesis: ( a in (<=6n+1 m) /\ SetPrimes implies a <= (6 * m) + 1 )
assume a in (<=6n+1 m) /\ SetPrimes ; :: thesis: a <= (6 * m) + 1
then a in <=6n+1 m by XBOOLE_0:def 4;
hence a <= (6 * m) + 1 by Th7; :: thesis: verum

end;

hence (6 * m) + 1 = LP<=6n+1 m by A3, XXREAL_2:def 8; :: thesis: verum