theorem :: PSCOMP_1:6

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