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