theorem :: TOPREAL6:37

for P being Subset of (TOP-REAL 2) holds LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P)