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