set A = <=6n+1 1;
set X = (<=6n+1 1) /\ SetPrimes;
A1: 7 in <=6n+1 1 ;
7 in SetPrimes by XPRIMES1:7, NEWTON:def 6;
then A2: 7 in (<=6n+1 1) /\ SetPrimes by A1, XBOOLE_0:def 4;

now :: thesis: for x being ExtReal st x in (<=6n+1 1) /\ SetPrimes holds
x <= 7

let x be ExtReal; :: thesis: ( x in (<=6n+1 1) /\ SetPrimes implies x <= 7 )
assume x in (<=6n+1 1) /\ SetPrimes ; :: thesis: x <= 7
then x in <=6n+1 1 by XBOOLE_0:def 4;
then ex a being Nat st
( a = x & a <= (6 * 1) + 1 ) ;
hence x <= 7 ; :: thesis: verum

end;

hence LP<=6n+1 1 = 7 by A2, XXREAL_2:def 8; :: thesis: verum