for X, Y being set
for f being real-valued Function holds
( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )