theorem Th22: :: RCOMP_1:22

for X being Subset of REAL st X is open & X is bounded_below holds
not lower_bound X in X