let s1, s2, t1, t2 be Real; :: thesis: { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } is Subset of (REAL 2)
{ |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } c= REAL 2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } or y in REAL 2 )
assume y in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } ; :: thesis: y in REAL 2
then consider s7, t7 being Real such that
W: ( |[s7,t7]| = y & ( not s1 <= s7 or not s7 <= s2 or not t1 <= t7 or not t7 <= t2 ) ) ;
|[s7,t7]| in the carrier of (TOP-REAL 2) ;
then |[s7,t7]| in REAL 2 by EUCLID:25;
hence y in REAL 2 by W; :: thesis: verum

end;

hence { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } is Subset of (REAL 2) ; :: thesis: verum