let A be ext-real-membered set ; :: thesis: ( sup A = inf A implies A = {(inf A)} )
assume Z: sup A = inf A ; :: thesis: A = {(inf A)}
then A c= [.(inf A),(inf A).] by Th73;
then A: A c= {(inf A)} by XXREAL_1:17;
A <> {} by Z, TW3, TW4;
hence A = {(inf A)} by A, ZFMISC_1:39; :: thesis: verum