let C be non empty compact Subset of (TOP-REAL 2); :: thesis: W-max (L~ (SpStSeq C)) = NW-corner C
set X = L~ (SpStSeq C);
set S = W-most (L~ (SpStSeq C));
A1: W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C)) by Th66;
A2: S-bound C <= N-bound C by Th22;
upper_bound (proj2 | (W-most (L~ (SpStSeq C)))) = upper_bound (rng (proj2 | (W-most (L~ (SpStSeq C))))) by RELSET_1:22
.= upper_bound (proj2 .: (W-most (L~ (SpStSeq C)))) by RELAT_1:115
.= upper_bound [.(S-bound C),(N-bound C).] by A1, Th70
.= N-bound C by A2, JORDAN5A:19 ;
hence W-max (L~ (SpStSeq C)) = NW-corner C by Th58; :: thesis: verum