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: 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;
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 Th41;
then A2: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) c= L~ (SpStSeq C) by XBOOLE_1:7;
LSeg ((SW-corner (L~ (SpStSeq C))),(NW-corner (L~ (SpStSeq C)))) = LSeg ((SW-corner (L~ (SpStSeq C))),(NW-corner C)) by Th62
.= LSeg ((SW-corner C),(NW-corner C)) by Th64 ;
hence W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C)) by A1, A2, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum