theorem Th23: :: SPRECT_1:23

for C being non empty compact Subset of (TOP-REAL 2) holds LSeg ((SE-corner C),(NE-corner C)) = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) }