theorem :: TOPREAL6:35

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