let C be non empty compact Subset of (TOP-REAL 2); :: thesis: E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C))
set X = L~ (SpStSeq C);
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
A1: LSeg ((NE-corner C),(SE-corner C)) c= (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-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 ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) c= L~ (SpStSeq C) by XBOOLE_1:7;
LSeg ((SE-corner (L~ (SpStSeq C))),(NE-corner (L~ (SpStSeq C)))) = LSeg ((SE-corner (L~ (SpStSeq C))),(NE-corner C)) by Th63
.= LSeg ((SE-corner C),(NE-corner C)) by Th65 ;
hence E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C)) by A1, A2, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum