let s1, s2, t1, t2 be Real; { pq where pq is Point of : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } is Subset of
{ |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } is Subset of
by Lm2, Lm8;
hence
{ pq where pq is Point of : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } is Subset of
by Th33; verum