let P be Subset of R^1; :: thesis: for r, s being real number st P = ].r,s.[ holds
P is open
let r, s be real number ; :: 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 set ; :: 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 ex r1 being Real st
( r1 = x & r < r1 ) ;
hence x in REAL ; :: 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 set ; :: 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 ex r2 being Real st
( r2 = x & s > r2 ) ;
hence x in REAL ; :: thesis: verum

end;

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

proof

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

end;

P1 /\ P2 c= P

proof

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

end;

then P = P1 /\ P2 by A4, XBOOLE_0:def 10;
hence P is open by A2, A3, TOPS_1:11; :: thesis: verum