let s1, t1, s2, t2 be Real; :: thesis: for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds
P is open
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } implies P is open )
assume A1: P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } ; :: thesis: P is open
reconsider P1 = { |[s,t]| where s, t is Real : s1 < s } as Subset of (TOP-REAL 2) by Lm4, XX;
reconsider P2 = { |[s,t]| where s, t is Real : s < s2 } as Subset of (TOP-REAL 2) by Lm2, XX;
reconsider P3 = { |[s,t]| where s, t is Real : t1 < t } as Subset of (TOP-REAL 2) by Lm5, XX;
reconsider P4 = { |[s,t]| where s, t is Real : t < t2 } as Subset of (TOP-REAL 2) by Lm3, XX;
A2: P = ((P1 /\ P2) /\ P3) /\ P4 by A1, Th12;
( P1 is open & P2 is open ) by Th25, Th26;
then A3: P1 /\ P2 is open by TOPS_1:38;
A4: ( P3 is open & P4 is open ) by Th27, Th28;
then (P1 /\ P2) /\ P3 is open by A3, TOPS_1:38;
hence P is open by A2, A4, TOPS_1:38; :: thesis: verum