theorem :: RFUNCT_1:81

for X being set
for f being real-valued Function holds (abs f) | X is bounded_below ;