let C be non empty compact Subset of (TOP-REAL 2); :: thesis: W-most (L~ (SpStSeq C)) = LSeg (SW-corner C),(NW-corner C)
set X = L~ (SpStSeq C);
set S3 = LSeg (SE-corner C),(SW-corner C);
set S4 = LSeg (SW-corner C),(NW-corner C);
A1: L~ (SpStSeq 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 Th43;
A2: LSeg (SW-corner C),(NW-corner C) c= (LSeg (SE-corner C),(SW-corner C)) \/ (LSeg (SW-corner C),(NW-corner C)) by XBOOLE_1:7;
A3: (LSeg (SE-corner C),(SW-corner C)) \/ (LSeg (SW-corner C),(NW-corner C)) c= L~ (SpStSeq C) by A1, XBOOLE_1:7;
LSeg (SW-corner (L~ (SpStSeq C))),(NW-corner (L~ (SpStSeq C))) = LSeg (SW-corner (L~ (SpStSeq C))),(NW-corner C) by Th70
.= LSeg (SW-corner C),(NW-corner C) by Th72 ;
hence W-most (L~ (SpStSeq C)) = LSeg (SW-corner C),(NW-corner C) by A2, A3, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum