let s1, t1, s2, t2 be Real; { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } is open Subset of (TOP-REAL 2)
set P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } ;
A1:
{ |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } = (( { |[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 Th7;
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 Th15;
A1 is open
by Th17;
then A3:
A0 \/ A1 is open
by A2, TOPS_1:10;
A2 is open
by Th14;
then A4:
(A0 \/ A1) \/ A2 is open
by A3, TOPS_1:10;
A3 is open
by Th16;
hence
{ |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } is open Subset of (TOP-REAL 2)
by A1, A4, TOPS_1:10; verum