let P be Subset of R^1; :: thesis: for a being Real st P = { s where s is Real : a < s } holds
P is open
let a be Real; :: thesis: ( P = { s where s is Real : a < s } implies P is open )
assume A1: P = { s where s is Real : a < s } ; :: thesis: P is open
for c being Point of RealSpace st c in P holds
ex r being Real st
( r > 0 & Ball (c,r) c= P )

proof

let c be Point of RealSpace; :: thesis: ( c in P implies ex r being Real st
( r > 0 & Ball (c,r) c= P ) )
reconsider n = c as Element of REAL by METRIC_1:def 13;
reconsider r = n - a as Real ;
assume c in P ; :: thesis: ex r being Real st
( r > 0 & Ball (c,r) c= P )
then A2: ex s being Real st
( s = n & a < s ) by A1;
take r ; :: thesis: ( r > 0 & Ball (c,r) c= P )

now :: thesis: for x being object st x in Ball (c,r) holds
x in P

let x be object ; :: thesis: ( x in Ball (c,r) implies x in P )
assume A3: x in Ball (c,r) ; :: thesis: x in P
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A3;
Ball (c,r) = { q where q is Element of RealSpace : dist (c,q) < r } by METRIC_1:17;
then ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A3;
then real_dist . (n,t) < r by METRIC_1:def 1, METRIC_1:def 13;
then A4: |.(n - t).| < r by METRIC_1:def 12;
n - t <= |.(n - t).| by ABSVALUE:4;
then n - t < n - a by A4, XXREAL_0:2;
then a < t by XREAL_1:10;
hence x in P by A1; :: thesis: verum

end;

hence ( r > 0 & Ball (c,r) c= P ) by A2, XREAL_1:50; :: thesis: verum

end;

hence P is open by TOPMETR:15, TOPMETR:def 6; :: thesis: verum