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