let P be Subset of R^1; :: thesis: for r, s being Real st P = ].r,s.[ holds
P is open
let r, s be Real; :: thesis: ( P = ].r,s.[ implies P is open )
assume A1: P = ].r,s.[ ; :: thesis: P is open
{ r1 where r1 is Real : r < r1 } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r1 where r1 is Real : r < r1 } or x in REAL )
assume x in { r1 where r1 is Real : r < r1 } ; :: thesis: x in REAL
then consider r1 being Real such that
A2: ( r1 = x & r < r1 ) ;
r1 in REAL by XREAL_0:def 1;
hence x in REAL by A2; :: thesis: verum

end;

then reconsider P1 = { r1 where r1 is Real : r < r1 } as Subset of R^1 by TOPMETR:17;
{ r2 where r2 is Real : s > r2 } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r2 where r2 is Real : s > r2 } or x in REAL )
assume x in { r2 where r2 is Real : s > r2 } ; :: thesis: x in REAL
then consider r2 being Real such that
A3: ( r2 = x & s > r2 ) ;
r2 in REAL by XREAL_0:def 1;
hence x in REAL by A3; :: thesis: verum

end;

then reconsider P2 = { r2 where r2 is Real : s > r2 } as Subset of R^1 by TOPMETR:17;
A4: P1 is open by JORDAN2B:25;
A5: P2 is open by JORDAN2B:24;
A6: P c= P1 /\ P2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in P1 /\ P2 )
assume A7: x in P ; :: thesis: x in P1 /\ P2
then reconsider r1 = x as Real ;
A8: r < r1 by A1, A7, XXREAL_1:4;
A9: r1 < s by A1, A7, XXREAL_1:4;
A10: x in P1 by A8;
x in P2 by A9;
hence x in P1 /\ P2 by A10, XBOOLE_0:def 4; :: thesis: verum

end;

P1 /\ P2 c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 /\ P2 or x in P )
assume A11: x in P1 /\ P2 ; :: thesis: x in P
then A12: x in P1 by XBOOLE_0:def 4;
A13: x in P2 by A11, XBOOLE_0:def 4;
A14: ex r1 being Real st
( r1 = x & r < r1 ) by A12;
ex r2 being Real st
( r2 = x & s > r2 ) by A13;
hence x in P by A1, A14, XXREAL_1:4; :: thesis: verum

end;

then P = P1 /\ P2 by A6;
hence P is open by A4, A5, TOPS_1:11; :: thesis: verum