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