theorem Th28: :: JORDAN1:34

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } holds
P is open