theorem Th43: :: SEQ_4:43

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