let P be Subset of (TOP-REAL 2); for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } holds
P is open
deffunc H1( Real, Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,$2]|;
let r3, q3 be Real; ( P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } implies P is open )
defpred S1[ Real, Real] means r3 < $2;
defpred S2[ 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 ) }
; P is open
then A5:
P = Q1 /\ Q2
by TARSKI:2;
thus
P is open
by A5, TOPS_1:11; verum