let s1, t1, s2, t2 be Real; :: thesis: for P being Subset of st P = { 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 ) } holds
P is connected
let P be Subset of ; :: thesis: ( P = { 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 ) } implies P is connected )
assume P = { 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 ) } ; :: thesis: P is connected
then P = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } by Th33;
hence P is connected by Th24; :: thesis: verum