let Y, X 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 A2: ( Y c= X & f | X is bounded_above ) ; :: thesis: f | Y is bounded_above
then consider r being real number such that
A3: for c being set st c in X /\ (dom f) holds
f . c <= r by Def9;

now

take r = r; :: thesis: for c being set st c in Y /\ (dom f) holds
f . c <= r
let c be set ; :: thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume c in Y /\ (dom f) ; :: thesis: f . c <= r
then ( c in Y & c in dom f ) by XBOOLE_0:def 4;
then c in X /\ (dom f) by A2, XBOOLE_0:def 4;
hence f . c <= r by A3; :: thesis: verum

end;

hence f | Y is bounded_above by Def9; :: thesis: verum

end;

thus A4: ( 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 A5: ( Y c= X & f | X is bounded_below ) ; :: thesis: f | Y is bounded_below
then consider r being real number such that
A6: for c being set st c in X /\ (dom f) holds
r <= f . c by Def10;

now

take r = r; :: thesis: for c being set st c in Y /\ (dom f) holds
r <= f . c
let c be set ; :: thesis: ( c in Y /\ (dom f) implies r <= f . c )
assume c in Y /\ (dom f) ; :: thesis: r <= f . c
then ( c in Y & c in dom f ) by XBOOLE_0:def 4;
then c in X /\ (dom f) by A5, XBOOLE_0:def 4;
hence r <= f . c by A6; :: thesis: verum

end;

hence f | Y is bounded_below by Def10; :: thesis: verum

end;

assume ( Y c= X & f | X is bounded ) ; :: thesis: f | Y is bounded
hence f | Y is bounded by A1, A4; :: thesis: verum