let C be non empty set ; :: thesis: for X being set
for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
let X be set ; :: thesis: for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
let f be PartFunc of C,REAL; :: thesis: (max+ f) | X is bounded_below
for c being object st c in X /\ (dom (max+ f)) holds
(max+ f) . c >= 0 by RFUNCT_3:37;
hence (max+ f) | X is bounded_below by RFUNCT_1:71; :: thesis: verum