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 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;
A2: P = ((P1 /\ P2) /\ P3) /\ P4 by A1, Th12;
A3: P1 is open by Th25;
P2 is open by Th26;
then A4: P1 /\ P2 is open by A3, TOPS_1:11;
A5: P3 is open by Th27;
A6: P4 is open by Th28;
(P1 /\ P2) /\ P3 is open by A4, A5, TOPS_1:11;
hence P is open by A2, A6, TOPS_1:11; :: thesis: verum