let C be non empty compact Subset of (TOP-REAL 2); :: thesis: S-min (L~ (SpStSeq C)) = SW-corner C
set X = L~ (SpStSeq C);
set S = S-most (L~ (SpStSeq C));
A1: S-most (L~ (SpStSeq C)) = LSeg (SW-corner C),(SE-corner C) by Th76;
A2: W-bound C <= E-bound C by Th23;
inf (proj1 | (S-most (L~ (SpStSeq C)))) = inf (rng (proj1 | (S-most (L~ (SpStSeq C))))) by FUNCT_2:45
.= inf (proj1 .: (S-most (L~ (SpStSeq C)))) by RELAT_1:148
.= inf [.(W-bound C),(E-bound C).] by A1, Th81
.= W-bound C by A2, JORDAN5A:20 ;
hence S-min (L~ (SpStSeq C)) = SW-corner C by Th67; :: thesis: verum