theorem :: XXREAL_2:70

for A being ext-real-membered set st sup A = inf A holds
A = {(inf A)}