let P be Subset of (TOP-REAL 2); LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P)
LSeg ((SW-corner P),(NW-corner P)) c= (((LSeg ((NW-corner P),(NE-corner P))) \/ (LSeg ((NE-corner P),(SE-corner P)))) \/ (LSeg ((SE-corner P),(SW-corner P)))) \/ (LSeg ((SW-corner P),(NW-corner P)))
by XBOOLE_1:7;
then
LSeg ((SW-corner P),(NW-corner P)) c= ((LSeg ((NW-corner P),(NE-corner P))) \/ (LSeg ((NE-corner P),(SE-corner P)))) \/ ((LSeg ((SE-corner P),(SW-corner P))) \/ (LSeg ((SW-corner P),(NW-corner P))))
by XBOOLE_1:4;
hence
LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P)
by SPRECT_1:41; verum