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

{ r2 where r2 is Real : s > r2 } c= REAL

A4: P1 is open by JORDAN2B:25;

A5: P2 is open by JORDAN2B:24;

A6: P c= P1 /\ P2

hence P is open by A4, A5, TOPS_1:11; :: thesis: verum

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

then reconsider P1 = { r1 where r1 is Real : r < r1 } as Subset of R^1 by TOPMETR:17;
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;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

{ r2 where r2 is Real : s > r2 } c= REAL

proof

then reconsider P2 = { r2 where r2 is Real : s > r2 } as Subset of R^1 by TOPMETR:17;
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;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

A4: P1 is open by JORDAN2B:25;

A5: P2 is open by JORDAN2B:24;

A6: P c= P1 /\ P2

proof

P1 /\ P2 c= P
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;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

proof

then
P = P1 /\ P2
by A6;
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;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

hence P is open by A4, A5, TOPS_1:11; :: thesis: verum