let P be Subset of (TOP-REAL 2); :: thesis:
deffunc H₁( Real, Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,$2]|;
let r3, q3 be Real; :: thesis:
defpred S₁[ Real, Real] means r3 < $2;
defpred S₂[ Real, Real] means $2 < q3;
reconsider Q1 = { |[r1,r2]| where r1, r2 is Real : r3 < r2 } , Q2 = { |[r1,r2]| where r1, r2 is Real : r2 < q3 } as open Subset of (TOP-REAL 2) by JORDAN1:22, JORDAN1:23;
assume A1: P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } ; :: thesis:

end;

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

end;