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