let P be Subset of R^1 ; :: thesis: for a being real number st P = { s where s is Real : a < s } holds
P is open
let a be real number ; :: 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 number st
( r > 0 & Ball c,r c= P )

proof

let c be Point of RealSpace ; :: thesis: ( c in P implies ex r being real number st
( r > 0 & Ball c,r c= P ) )
reconsider n = c as Real by METRIC_1:def 14;
reconsider r = n - a as Real ;
assume c in P ; :: thesis: ex r being real number 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

let x be set ; :: 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 Real by METRIC_1:def 14;
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:18;
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 14;
then A4: abs (n - t) < r by METRIC_1:def 13;
n - t <= abs (n - t) by ABSVALUE:11;
then n - t < n - a by A4, XXREAL_0:2;
then a < t by XREAL_1:12;
hence x in P by A1; :: thesis: verum

end;

hence ( r > 0 & Ball c,r c= P ) by A2, TARSKI:def 3, XREAL_1:52; :: thesis: verum

end;

hence P is open by TOPMETR:22, TOPMETR:def 7; :: thesis: verum