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