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 ) )
assume A2: c in P ; :: thesis: ex r being real number st
( r > 0 & Ball c,r c= P )
reconsider n = c as Real by METRIC_1:def 14;
consider s being Real such that
A3: ( s = n & s < b ) by A1, A2;
reconsider r = b - n as Real ;
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 A4: 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 A4;
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 A4;
then real_dist . t,n < r by METRIC_1:def 1, METRIC_1:def 14;
then ( abs (t - n) < r & t - n <= abs (t - n) ) by ABSVALUE:11, METRIC_1:def 13;
then t - n < b - n by XXREAL_0:2;
then t < b by XREAL_1:11;
hence x in P by A1; :: thesis: verum

end;

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

end;

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