theorem Th21: :: JORDAN1:27

for s1, s2, t1, t2 being Real holds { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) }