theorem Th25: :: JORDAN1:31

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