theorem :: PSCOMP_1:5

for T being non empty TopSpace
for f being bounded_above RealMap of T
for t being Real st ( for p being Point of T holds f . p <= t ) holds
upper_bound f <= t