let X, Y be set ; :: thesis: for f being real-valued Function st f | X is bounded_above & f | Y is bounded_below holds
f | (X /\ Y) is bounded
let f be real-valued Function; :: thesis: ( f | X is bounded_above & f | Y is bounded_below implies f | (X /\ Y) is bounded )
assume A1: ( f | X is bounded_above & f | Y is bounded_below ) ; :: thesis: f | (X /\ Y) is bounded
then consider r1 being real number such that
A2: for c being set st c in X /\ (dom f) holds
f . c <= r1 by Def9;
consider r2 being real number such that
A3: for c being set st c in Y /\ (dom f) holds
r2 <= f . c by A1, Def10;

now

let c be set ; :: thesis: ( c in (X /\ Y) /\ (dom f) implies f . c <= r1 )
assume c in (X /\ Y) /\ (dom f) ; :: thesis: f . c <= r1
then ( c in X /\ Y & c in dom f ) by XBOOLE_0:def 4;
then ( c in X & c in dom f ) by XBOOLE_0:def 4;
then c in X /\ (dom f) by XBOOLE_0:def 4;
hence f . c <= r1 by A2; :: thesis: verum

end;

hence f | (X /\ Y) is bounded_above by Def9; :: according to SEQ_2:def 8 :: thesis: f | (X /\ Y) is bounded_below

now

let c be set ; :: thesis: ( c in (X /\ Y) /\ (dom f) implies r2 <= f . c )
assume c in (X /\ Y) /\ (dom f) ; :: thesis: r2 <= f . c
then ( c in X /\ Y & c in dom f ) by XBOOLE_0:def 4;
then ( c in Y & c in dom f ) by XBOOLE_0:def 4;
then c in Y /\ (dom f) by XBOOLE_0:def 4;
hence r2 <= f . c by A3; :: thesis: verum

end;

hence f | (X /\ Y) is bounded_below by Def10; :: thesis: verum