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 A2: ( U1 in B & U2 in B & 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
A3: ( U1 = [.x1,q1.[ & x1 < q1 & q1 is rational ) by A2;
consider x2, q2 being Element of REAL such that
A4: ( U2 = [.x2,q2.[ & x2 < q2 & q2 is rational ) by A2;
A5: ( x in U1 & x in U2 ) by A2, XBOOLE_0:def 4;
then reconsider x' = x as Element of REAL by A3;
A6: ( x1 <= x' & x2 <= x' & x' < q1 & x' < q2 ) by A3, A4, A5, XXREAL_1:3;
set y = max x1,x2;
set q = min q1,q2;
( x2 < q1 & x1 < q2 ) by A6, XXREAL_0:2;
then ( max x1,x2 < q1 & max x1,x2 < q2 & x1 <= max x1,x2 & x2 <= max x1,x2 & min q1,q2 <= q1 & min q1,q2 <= q2 ) by A3, A4, XXREAL_0:17, XXREAL_0:29, XXREAL_0:31;
then ( max x1,x2 < min q1,q2 & min q1,q2 is rational & [.(max x1,x2),(min q1,q2).[ c= U1 & [.(max x1,x2),(min q1,q2).[ c= U2 & max x1,x2 <= x' & x' < min q1,q2 ) by A3, A4, A6, XXREAL_0:15, XXREAL_0:28, XXREAL_1:38;
then ( x' in [.(max x1,x2),(min q1,q2).[ & [.(max x1,x2),(min q1,q2).[ in B & [.(max x1,x2),(min q1,q2).[ c= U1 /\ U2 ) by XBOOLE_1:19, XXREAL_1:3;
hence ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 ) ; :: 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 x' = x as Element of REAL ;
x' + 0 < x' + 1 by XREAL_1:8;
then consider q being rational number such that
A7: ( x' < q & q < x' + 1 ) by RAT_1:22;
take U = [.x',q.[; :: thesis: ( U in B & x in U )
q in REAL by XREAL_0:def 1;
hence U in B by A7; :: thesis: x in U
thus x in U by A7, 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