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

let U be Subset of R^1; :: thesis: ( U is open implies for x being Point of R^1 st x in U holds
ex V being Subset of R^1 st
( V in X & x in V & V c= U ) )
assume A2: U is open ; :: thesis: for x being Point of R^1 st x in U holds
ex V being Subset of R^1 st
( V in X & x in V & V c= U )
let x be Point of R^1; :: thesis: ( x in U implies ex V being Subset of R^1 st
( V in X & x in V & V c= U ) )
assume A3: x in U ; :: thesis: ex V being Subset of R^1 st
( V in X & x in V & V c= U )
reconsider a = x as Real ;
consider r being Real such that
A4: 0 < r and
A5: ].(a - r),(a + r).[ c= U by A2, A3, FRECHET:8;
reconsider V = ].(a - r),(a + r).[ as Subset of R^1 by TOPMETR:17;
take V = V; :: thesis: ( V in X & x in V & V c= U )
A6: a < a + r by A4, XREAL_1:29;
A7: a - r < a by A4, XREAL_1:44;
then a - r < a + r by A6, XXREAL_0:2;
hence V in X ; :: thesis: ( x in V & V c= U )
thus x in V by A7, A6, XXREAL_1:4; :: thesis: V c= U
thus V c= U by A5; :: thesis: verum

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in X or u in the topology of R^1 )
assume u in X ; :: thesis: u in the topology of R^1
then ex a, b being Real st
( u = ].a,b.[ & a < b ) ;
then u is open Subset of R^1 by JORDAN6:35, TOPMETR:17;
hence u in the topology of R^1 by PRE_TOPC:def 2; :: thesis: verum