for r being Real
for X being non empty real-membered set st ( for s being Real st s in X holds
s >= r ) & ( for t being Real st ( for s being Real st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X by Lm1;