theorem Th13: :: RCOMP_1:13

for X being Subset of REAL st X <> {} & X is closed & X is bounded_below holds
lower_bound X in X