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 : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds
P is open
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } implies P is open )
assume P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } ; :: thesis: P is open
then A1: P = (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } by Th13;
reconsider A0 = { |[s,t]| where s, t is Real : s < s1 } as Subset of (TOP-REAL 2) by Lm2, Lm3;
reconsider A1 = { |[s,t]| where s, t is Real : t < t1 } as Subset of (TOP-REAL 2) by Lm2, Lm4;
reconsider A2 = { |[s,t]| where s, t is Real : s2 < s } as Subset of (TOP-REAL 2) by Lm2, Lm5;
reconsider A3 = { |[s,t]| where s, t is Real : t2 < t } as Subset of (TOP-REAL 2) by Lm2, Lm6;
A2: A0 is open by Th26;
A1 is open by Th28;
then A3: A0 \/ A1 is open by A2, TOPS_1:10;
A2 is open by Th25;
then A4: (A0 \/ A1) \/ A2 is open by A3, TOPS_1:10;
A3 is open by Th27;
hence P is open by A1, A4, TOPS_1:10; :: thesis: verum