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;

consider r2 being Real such that

A6: for c being object st c in Y /\ (dom f) holds

r2 <= f . c by A2, Th71;

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

hence
f | (X /\ Y) is bounded_above
by Th70; :: according to SEQ_2:def 8 :: thesis: f | (X /\ Y) is bounded_below 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;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

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

hence
f | (X /\ Y) is bounded_below
by Th71; :: thesis: verumr2 <= 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;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