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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } or a in bool REAL )
assume a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ; :: thesis: a in bool REAL
then ex x, q being Element of 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 Element of 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 Element of REAL such that
A5: U1 = [.x1,q1.[ and
A6: x1 < q1 and
A7: q1 is rational by A2;
consider x2, q2 being Element of 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

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:8;
then consider q being rational number such that
A25: x9 < q and
q < x9 + 1 by RAT_1:22;
take U = [.x9,q.[; :: thesis: ( U in B & x in U )
q in REAL by XREAL_0:def 1;
hence 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 Element of REAL : ( x < q & q is rational ) } ) ) ; :: thesis: verum