let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( S-min X = S-max X implies S-most X = {(S-min X)} )
assume S-min X = S-max X ; :: thesis: S-most X = {(S-min X)}
then S-most X c= LSeg ((S-min X),(S-min X)) by Th56;
then S-most X c= {(S-min X)} by RLTOPSP1:70;
hence S-most X = {(S-min X)} by ZFMISC_1:33; :: thesis: verum