let X be non empty real-membered set ; :: thesis: ( ( for r being Real st r in X holds
upper_bound X = r ) implies ex r being Real st X = {r} )
assume A1: for r being Real st r in X holds
upper_bound X = r ; :: thesis: ex r being Real st X = {r}
ex s being object st
for x being object st x in X holds
s = x

proof

set s = upper_bound X;
take upper_bound X ; :: thesis: for x being object st x in X holds
upper_bound X = x
thus for x being object st x in X holds
upper_bound X = x by A1; :: thesis: verum

end;

then consider r being object such that
A2: X = {r} by Lm03;
reconsider r0 = the Element of X as Real ;
take r0 ; :: thesis: X = {r0}
thus X = {r0} by A2, TARSKI:def 1; :: thesis: verum