let P be Subset of (TOP-REAL 2); :: thesis: for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } holds
P is open
let r3, q3 be Real; :: thesis: ( P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } implies P is open )
assume A1: P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } ; :: thesis: P is open
deffunc H₁( Real, Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,$2]|;
defpred S₁[ Real, Real] means r3 < $2;
defpred S₂[ Real, Real] means $2 < q3;
A2: { H₁(r1,r2) where r1, r2 is Real : S₁[r1,r2] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 9();
{ H₁(r1,r2) where r1, r2 is Real : S₂[r1,r2] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 9();
then reconsider Q1 = { |[r1,r2]| where r1, r2 is Real : r3 < r2 } , Q2 = { |[r1,r2]| where r1, r2 is Real : r2 < q3 } as Subset of (TOP-REAL 2) by A2;
A3: Q1 is open by JORDAN1:27;
A4: Q2 is open by JORDAN1:28;

now

let x be set ; :: thesis: ( ( x in P implies x in Q1 /\ Q2 ) & ( x in Q1 /\ Q2 implies x in P ) )

hereby :: thesis: ( x in Q1 /\ Q2 implies x in P )

assume x in P ; :: thesis: x in Q1 /\ Q2
then consider r1, r2 being Real such that
A5: ( x = |[r1,r2]| & r3 < r2 & r2 < q3 ) by A1;
( x in Q1 & x in Q2 ) by A5;
hence x in Q1 /\ Q2 by XBOOLE_0:def 4; :: thesis: verum

end;

assume x in Q1 /\ Q2 ; :: thesis: x in P
then A6: ( x in Q1 & x in Q2 ) by XBOOLE_0:def 4;
then consider r1, r2 being Real such that
A7: ( x = |[r1,r2]| & r3 < r2 ) ;
consider r1', r2' being Real such that
A8: ( x = |[r1',r2']| & r2' < q3 ) by A6;
( |[r1,r2]| `1 = r1 & |[r1,r2]| `2 = r2 & |[r1',r2']| `1 = r1' & |[r1',r2']| `2 = r2' ) by EUCLID:56;
hence x in P by A1, A7, A8; :: thesis: verum

end;

then P = Q1 /\ Q2 by TARSKI:2;
hence P is open by A3, A4, TOPS_1:38; :: thesis: verum