let P be Subset of (TOP-REAL 2); :: thesis: for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } holds
P is open
deffunc H₁( Real, Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,$2]|;
let r3, q3 be Real; :: thesis: ( P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } implies P is open )
defpred S₁[ Real, Real] means r3 < $1;
defpred S₂[ Real, Real] means $1 < q3;
A1: { 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 < r1 } , Q2 = { |[r1,r2]| where r1, r2 is Real : r1 < q3 } as Subset of (TOP-REAL 2) by A1;
assume A2: P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } ; :: thesis: P is open

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 ex r1, r2 being Real st
( x = |[r1,r2]| & r3 < r1 & r1 < q3 ) by A2;
then ( x in Q1 & x in Q2 ) ;
hence x in Q1 /\ Q2 by XBOOLE_0:def 4; :: thesis: verum

end;

assume A3: x in Q1 /\ Q2 ; :: thesis: x in P
then x in Q1 by XBOOLE_0:def 4;
then consider r1, r2 being Real such that
A4: ( x = |[r1,r2]| & r3 < r1 ) ;
x in Q2 by A3, XBOOLE_0:def 4;
then consider r19, r29 being Real such that
A5: ( x = |[r19,r29]| & r19 < q3 ) ;
( |[r1,r2]| `1 = r1 & |[r19,r29]| `1 = r19 ) by EUCLID:52;
hence x in P by A2, A4, A5; :: thesis: verum

end;

then A6: P = Q1 /\ Q2 by TARSKI:1;
( Q1 is open & Q2 is open ) by JORDAN1:20, JORDAN1:21;
hence P is open by A6, TOPS_1:11; :: thesis: verum