for X being ext-real-membered non empty set
for x being LowerBound of X st x in X holds
x = inf X