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: 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 (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;
A3: (LSeg (NW-corner C),(NE-corner C)) \/ (LSeg (NE-corner C),(SE-corner C)) c= L~ (SpStSeq C) by A1, XBOOLE_1:7;
LSeg (SE-corner (L~ (SpStSeq C))),(NE-corner (L~ (SpStSeq C))) = LSeg (SE-corner (L~ (SpStSeq C))),(NE-corner C) by Th71
.= LSeg (SE-corner C),(NE-corner C) by Th73 ;
hence E-most (L~ (SpStSeq C)) = LSeg (SE-corner C),(NE-corner C) by A2, A3, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum