theorem Th4: :: PSCOMP_1:4

for T being non empty TopSpace
for f being bounded_above RealMap of T
for p being Point of T holds f . p <= upper_bound f