let P be Subset of (TOP-REAL 2); :: thesis: 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; :: thesis: verum