let C be non empty compact Subset of (TOP-REAL 2); :: thesis: E-max (L~ (SpStSeq C)) = NE-corner C
set X = L~ (SpStSeq C);
set S = E-most (L~ (SpStSeq C));
A1: E-most (L~ (SpStSeq C)) = LSeg (SE-corner C),(NE-corner C) by Th77;
A2: S-bound C <= N-bound C by Th24;
sup (proj2 | (E-most (L~ (SpStSeq C)))) = sup (rng (proj2 | (E-most (L~ (SpStSeq C))))) by FUNCT_2:45
.= sup (proj2 .: (E-most (L~ (SpStSeq C)))) by RELAT_1:148
.= sup [.(S-bound C),(N-bound C).] by A1, Th80
.= N-bound C by A2, JORDAN5A:20 ;
hence E-max (L~ (SpStSeq C)) = NE-corner C by Th69; :: thesis: verum