let C be non empty compact Subset of (TOP-REAL 2); :: thesis: N-min (L~ (SpStSeq C)) = NW-corner C
set X = L~ (SpStSeq C);
set S = N-most (L~ (SpStSeq C));
A1: N-most (L~ (SpStSeq C)) = LSeg ((NW-corner C),(NE-corner C)) by Th67;
A2: W-bound C <= E-bound C by Th21;
lower_bound (proj1 | (N-most (L~ (SpStSeq C)))) = lower_bound (rng (proj1 | (N-most (L~ (SpStSeq C))))) by RELSET_1:22
.= lower_bound (proj1 .: (N-most (L~ (SpStSeq C)))) by RELAT_1:115
.= lower_bound [.(W-bound C),(E-bound C).] by A1, Th71
.= W-bound C by A2, JORDAN5A:19 ;
hence N-min (L~ (SpStSeq C)) = NW-corner C by Th60; :: thesis: verum