let s1, t1, s2, t2 be Real; :: thesis: { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } is open Subset of (TOP-REAL 2)
set P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } ;
reconsider P1 = { |[s,t]| where s, t is Real : s1 < s } as Subset of (TOP-REAL 2) by Lm2, Lm5;
reconsider P2 = { |[s,t]| where s, t is Real : s < s2 } as Subset of (TOP-REAL 2) by Lm2, Lm3;
reconsider P3 = { |[s,t]| where s, t is Real : t1 < t } as Subset of (TOP-REAL 2) by Lm2, Lm6;
reconsider P4 = { |[s,t]| where s, t is Real : t < t2 } as Subset of (TOP-REAL 2) by Lm2, Lm4;
A1: { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } = ((P1 /\ P2) /\ P3) /\ P4 by Th6;
A2: P1 is open by Th14;
P2 is open by Th15;
then A3: P1 /\ P2 is open by A2, TOPS_1:11;
A4: P3 is open by Th16;
A5: P4 is open by Th17;
(P1 /\ P2) /\ P3 is open by A3, A4, TOPS_1:11;
hence { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } is open Subset of (TOP-REAL 2) by A1, A5, TOPS_1:11; :: thesis: verum