theorem Th26: :: SPRECT_1:26

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