let P be Subset of (TOP-REAL 2); :: thesis: LSeg (SW-corner P),(SE-corner P) c= L~ (SpStSeq P)
((LSeg (NW-corner P),(NE-corner P)) \/ (LSeg (NE-corner P),(SE-corner P))) \/ (LSeg (SE-corner P),(SW-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 A1: ((LSeg (NW-corner P),(NE-corner P)) \/ (LSeg (NE-corner P),(SE-corner P))) \/ (LSeg (SE-corner P),(SW-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;
LSeg (SW-corner P),(SE-corner P) c= ((LSeg (NW-corner P),(NE-corner P)) \/ (LSeg (NE-corner P),(SE-corner P))) \/ (LSeg (SW-corner P),(SE-corner P)) by XBOOLE_1:7;
then LSeg (SW-corner P),(SE-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 A1, XBOOLE_1:1;
hence LSeg (SW-corner P),(SE-corner P) c= L~ (SpStSeq P) by SPRECT_1:43; :: thesis: verum