theorem :: PSCOMP_1:2

for T being non empty TopSpace
for f being bounded_below RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s