let A be ext-real-membered set ; :: thesis: ( sup A = inf A implies A = {(inf A)} )
assume A1: sup A = inf A ; :: thesis: A = {(inf A)}
then A c= [.(inf A),(inf A).] by Th69;
then A2: A c= {(inf A)} by XXREAL_1:17;
A <> {} by A1, Th38, Th39;
hence A = {(inf A)} by A2, ZFMISC_1:33; :: thesis: verum