let X be non empty real-membered set ; :: thesis: ( ( for r being Real st r in X holds
lower_bound X = r ) implies ex r being Real st X = {r} )
assume A1: for r being Real st r in X holds
lower_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 = lower_bound X;
take lower_bound X ; :: thesis: for x being object st x in X holds
lower_bound X = x
thus for x being object st x in X holds
lower_bound X = x by A1; :: thesis: verum

end;

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