set B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ;
{ [.x,q.[ where x, q is Real : ( x < q & q is rational ) } c= bool REAL

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } or a in bool REAL )
assume a in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ; :: thesis: a in bool REAL
then ex x, q being Real st
( a = [.x,q.[ & x < q & q is rational ) ;
hence a in bool REAL ; :: thesis: verum

end;

then reconsider B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } as Subset-Family of REAL ;
A1: B is point-filtered

proof

let x, U1, U2 be set ; :: according to TOPGEN_3:def 1 :: thesis: ( U1 in B & U2 in B & x in U1 /\ U2 implies ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 ) )
assume that
A2: U1 in B and
A3: U2 in B and
A4: x in U1 /\ U2 ; :: thesis: ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 )
consider x1, q1 being Real such that
A5: U1 = [.x1,q1.[ and
A6: x1 < q1 and
A7: q1 is rational by A2;
consider x2, q2 being Real such that
A8: U2 = [.x2,q2.[ and
A9: x2 < q2 and
A10: q2 is rational by A3;
set y = max (x1,x2);
set q = min (q1,q2);
A11: min (q1,q2) is rational by A7, A10, XXREAL_0:15;
A12: x in U1 by A4, XBOOLE_0:def 4;
then reconsider x9 = x as Element of REAL by A5;
A13: x in U2 by A4, XBOOLE_0:def 4;
then A14: x2 <= x9 by A8, XXREAL_1:3;
A15: x9 < q2 by A8, A13, XXREAL_1:3;
A16: min (q1,q2) <= q2 by XXREAL_0:17;
x2 <= max (x1,x2) by XXREAL_0:31;
then A17: [.(max (x1,x2)),(min (q1,q2)).[ c= U2 by A16, A8, XXREAL_1:38;
A18: min (q1,q2) <= q1 by XXREAL_0:17;
x1 <= max (x1,x2) by XXREAL_0:31;
then A19: [.(max (x1,x2)),(min (q1,q2)).[ c= U1 by A18, A5, XXREAL_1:38;
A20: x1 <= x9 by A5, A12, XXREAL_1:3;
then x1 < q2 by A15, XXREAL_0:2;
then A21: max (x1,x2) < q2 by A9, XXREAL_0:29;
A22: x9 < q1 by A5, A12, XXREAL_1:3;
then A23: x9 < min (q1,q2) by A15, XXREAL_0:15;
x2 < q1 by A14, A22, XXREAL_0:2;
then max (x1,x2) < q1 by A6, XXREAL_0:29;
then max (x1,x2) < min (q1,q2) by A21, XXREAL_0:15;
then A24: [.(max (x1,x2)),(min (q1,q2)).[ in B by A11;
max (x1,x2) <= x9 by A20, A14, XXREAL_0:28;
then x9 in [.(max (x1,x2)),(min (q1,q2)).[ by A23, XXREAL_1:3;
hence ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 ) by A24, A19, A17, XBOOLE_1:19; :: thesis: verum

end;

now :: thesis: for x being set st x in REAL holds
ex U being Element of bool REAL st
( U in B & x in U )

let x be set ; :: thesis: ( x in REAL implies ex U being Element of bool REAL st
( U in B & x in U ) )
assume x in REAL ; :: thesis: ex U being Element of bool REAL st
( U in B & x in U )
then reconsider x9 = x as Element of REAL ;
x9 + 0 < x9 + 1 by XREAL_1:6;
then consider q being Rational such that
A25: x9 < q and
q < x9 + 1 by RAT_1:7;
take U = [.x9,q.[; :: thesis: ( U in B & x in U )
thus U in B by A25; :: thesis: x in U
thus x in U by A25, XXREAL_1:3; :: thesis: verum

end;

then B is covering by Th1;
then TopStruct(# REAL,(UniCl B) #) is non empty TopSpace by A1, Th2;
hence ex b₁ being non empty strict TopSpace st
( the carrier of b₁ = REAL & ex B being Subset-Family of REAL st
( the topology of b₁ = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) ) ; :: thesis: verum