theorem Th70: :: RFUNCT_1:70

for Y being set
for f being real-valued Function holds
( f | Y is bounded_above iff ex r being Real st
for c being object st c in Y /\ (dom f) holds
f . c <= r )