let s1, t1, s2, t2 be Real; :: thesis: for P being Subset of st P = { p0 where p0 is Point of : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } holds
P is connected
let P be Subset of ; :: thesis: ( P = { p0 where p0 is Point of : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } implies P is connected )
assume P = { p0 where p0 is Point of : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } ; :: thesis: P is connected
then P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } by Th32;
hence P is connected by Th9, Th14; :: thesis: verum