set a = 20;
set b = 19;
set X = <=6n+1 20;
set A = LP<=6n+1 20;
set Y = <=6n+1 19;
set B = LP<=6n+1 19;
A1: LP<=6n+1 19 in SetPrimes by NEWTON:def 6;
LP<=6n+1 19 in (<=6n+1 19) /\ SetPrimes by XXREAL_2:def 8;
then LP<=6n+1 19 in <=6n+1 19 by XBOOLE_0:def 4;
then LP<=6n+1 19 <= (6 * 19) + 1 by Th7;
then LP<=6n+1 19 <= (6 * 20) + 1 by XXREAL_0:2;
then LP<=6n+1 19 in <=6n+1 20 ;
then A2: LP<=6n+1 19 in (<=6n+1 20) /\ SetPrimes by A1, XBOOLE_0:def 4;
for x being ExtReal st x in (<=6n+1 20) /\ SetPrimes holds
x <= LP<=6n+1 19

proof

let x be ExtReal; :: thesis: ( x in (<=6n+1 20) /\ SetPrimes implies x <= LP<=6n+1 19 )
assume A3: x in (<=6n+1 20) /\ SetPrimes ; :: thesis: x <= LP<=6n+1 19
A4: x in SetPrimes by A3, XBOOLE_0:def 4;
reconsider x = x as Nat by A3;

now :: thesis: not x > 115

assume x > 115 ; :: thesis: contradiction
then A5: x >= 115 + 1 by NAT_1:13;
x in <=6n+1 20 by A3, XBOOLE_0:def 4;
then x <= (6 * 20) + 1 by Th7;
then not not x = 116 + 0 & ... & not x = 116 + 5 by A5, NAT_1:62;
hence contradiction by A4, NEWTON:def 6, XPRIMES0:116, XPRIMES0:117, XPRIMES0:118, XPRIMES0:119, XPRIMES0:120, XPRIMES0:121; :: thesis: verum

end;

then x in <=6n+1 19 ;
then x in (<=6n+1 19) /\ SetPrimes by A4, XBOOLE_0:def 4;
hence x <= LP<=6n+1 19 by XXREAL_2:def 8; :: thesis: verum

end;

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