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;
reconsider Q1 = { |[r1,r2]| where r1, r2 is Real : r3 < r1 } , Q2 = { |[r1,r2]| where r1, r2 is Real : r1 < q3 } as open Subset of (TOP-REAL 2) by JORDAN1:20, JORDAN1:21;
assume A1: P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } ; :: thesis: P is open

now :: thesis: for x being object holds
( ( x in P implies x in Q1 /\ Q2 ) & ( x in Q1 /\ Q2 implies x in P ) )

let x be object ; :: 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
A2: ( x = |[r1,r2]| & r3 < r1 & r1 < q3 ) by A1;
( x in Q1 & x in Q2 ) by A2;
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 A1, A4, A5; :: thesis: verum

end;

then A6: P = Q1 /\ Q2 by TARSKI:2;
thus P is open by A6, TOPS_1:11; :: thesis: verum