theorem Th1: :: PSCOMP_1:1

for T being non empty TopSpace
for f being bounded_below RealMap of T
for p being Point of T holds f . p >= lower_bound f