let P be Subset of R^1; :: thesis: for b being real number st P = { s where s is Real : s < b } holds
P is open
let b be real number ; :: thesis: ( P = { s where s is Real : s < b } implies P is open )
assume A1: P = { s where s is Real : s < b } ; :: 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 13;
reconsider r = b - n 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 & s < b ) 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 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 . (t,n) < r by METRIC_1:def 1, METRIC_1:def 13;
then A4: abs (t - n) < r by METRIC_1:def 12;
t - n <= abs (t - n) by ABSVALUE:4;
then t - n < b - n by A4, XXREAL_0:2;
then t < b by XREAL_1:9;
hence x in P by A1; :: thesis: verum

end;

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

end;

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