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) c= (LSeg (NW-corner C),(NE-corner C)) \/ (LSeg (NE-corner C),(SE-corner C)) by XBOOLE_1:7;
(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;
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, XBOOLE_1:1;
hence LSeg (NW-corner C),(NE-corner C) c= L~ (SpStSeq C) by SPRECT_1:43; :: thesis: verum