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

A1: B is point-filtered

then TopStruct(# REAL,(UniCl B) #) is non empty TopSpace by A1, Th2;

hence ex b_{1} being non empty strict TopSpace st

( the carrier of b_{1} = REAL & ex B being Subset-Family of REAL st

( the topology of b_{1} = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) )
; :: thesis: verum

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

proof

then reconsider B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } as Subset-Family of REAL ;
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;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

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;( 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

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 )

then
B is covering
by Th1;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;( 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

then TopStruct(# REAL,(UniCl B) #) is non empty TopSpace by A1, Th2;

hence ex b

( the carrier of b

( the topology of b