let X be non empty real-membered bounded_below bounded_above set ; :: thesis: ( upper_bound X = lower_bound X implies ex r being Real st X = {r} )
assume A1: upper_bound X = lower_bound X ; :: thesis: ex r being Real st X = {r}
for r being Real st r in X holds
upper_bound X = r
proof
let r be Real; :: thesis: ( r in X implies upper_bound X = r )
assume r in X ; :: thesis: upper_bound X = r
then ( upper_bound X <= r & r <= upper_bound X ) by A1, SEQ_4:def 1, SEQ_4:def 2;
hence upper_bound X = r by XXREAL_0:1; :: thesis: verum
end;
hence ex r being Real st X = {r} by Th09; :: thesis: verum