theorem Th25: :: SPRECT_1:25

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