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 that
A1: f | X is bounded_above and
A2: f | Y is bounded_below ; :: thesis: f | (X /\ Y) is bounded
consider r1 being Real such that
A3: for c being object st c in X /\ (dom f) holds
f . c <= r1 by A1, Th70;

now :: thesis: for c being object st c in (X /\ Y) /\ (dom f) holds
f . c <= r1

let c be object ; :: thesis: ( c in (X /\ Y) /\ (dom f) implies f . c <= r1 )
assume A4: c in (X /\ Y) /\ (dom f) ; :: thesis: f . c <= r1
then c in X /\ Y by XBOOLE_0:def 4;
then A5: c in X by XBOOLE_0:def 4;
c in dom f by A4, XBOOLE_0:def 4;
then c in X /\ (dom f) by A5, XBOOLE_0:def 4;
hence f . c <= r1 by A3; :: thesis: verum

end;

hence f | (X /\ Y) is bounded_above by Th70; :: according to SEQ_2:def 8 :: thesis: f | (X /\ Y) is bounded_below
consider r2 being Real such that
A6: for c being object st c in Y /\ (dom f) holds
r2 <= f . c by A2, Th71;

now :: thesis: for c being object st c in (X /\ Y) /\ (dom f) holds
r2 <= f . c

let c be object ; :: thesis: ( c in (X /\ Y) /\ (dom f) implies r2 <= f . c )
assume A7: c in (X /\ Y) /\ (dom f) ; :: thesis: r2 <= f . c
then c in X /\ Y by XBOOLE_0:def 4;
then A8: c in Y by XBOOLE_0:def 4;
c in dom f by A7, XBOOLE_0:def 4;
then c in Y /\ (dom f) by A8, XBOOLE_0:def 4;
hence r2 <= f . c by A6; :: thesis: verum

end;

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