theorem Th7: :: PSCOMP_1:7

for T being non empty 1-sorted
for f being bounded RealMap of T holds lower_bound f <= upper_bound f