let X, Y be set ; :: thesis: 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 ) )

let f be real-valued Function; :: thesis: ( ( 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 ) )
thus A1: ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) :: thesis: ( ( 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 ) )
proof
assume that
A2: Y c= X and
A3: f | X is bounded_above ; :: thesis: f | Y is bounded_above
consider r being Real such that
A4: for c being object st c in X /\ (dom f) holds
f . c <= r by ;
now :: thesis: ex r being Real st
for c being object st c in Y /\ (dom f) holds
f . c <= r
take r = r; :: thesis: for c being object st c in Y /\ (dom f) holds
f . c <= r

let c be object ; :: thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume A5: c in Y /\ (dom f) ; :: thesis: f . c <= r
then A6: c in dom f by XBOOLE_0:def 4;
c in Y by ;
then c in X /\ (dom f) by ;
hence f . c <= r by A4; :: thesis: verum
end;
hence f | Y is bounded_above by Th70; :: thesis: verum
end;
thus A7: ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) :: thesis: ( Y c= X & f | X is bounded implies f | Y is bounded )
proof
assume that
A8: Y c= X and
A9: f | X is bounded_below ; :: thesis: f | Y is bounded_below
consider r being Real such that
A10: for c being object st c in X /\ (dom f) holds
r <= f . c by ;
now :: thesis: ex r being Real st
for c being object st c in Y /\ (dom f) holds
r <= f . c
take r = r; :: thesis: for c being object st c in Y /\ (dom f) holds
r <= f . c

let c be object ; :: thesis: ( c in Y /\ (dom f) implies r <= f . c )
assume A11: c in Y /\ (dom f) ; :: thesis: r <= f . c
then A12: c in dom f by XBOOLE_0:def 4;
c in Y by ;
then c in X /\ (dom f) by ;
hence r <= f . c by A10; :: thesis: verum
end;
hence f | Y is bounded_below by Th71; :: thesis: verum
end;
assume that
A13: Y c= X and
A14: f | X is bounded ; :: thesis: f | Y is bounded
thus f | Y is bounded by A1, A7, A13, A14; :: thesis: verum