:: deftheorem defines upper_bound PSCOMP_1:def 2 :
for T being 1-sorted
for f being RealMap of T holds upper_bound f = upper_bound (f .: the carrier of T);