for X being Subset of REAL
for r being Real st X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) holds
lower_bound X >= r