let Y be set ; :: thesis: for f being real-valued Function holds

( f | Y is bounded_above iff ex r being Real st

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

f . c <= r )

let f be real-valued Function; :: thesis: ( f | Y is bounded_above iff ex r being Real st

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

f . c <= r )

thus ( f | Y is bounded_above implies ex r being Real st

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

f . c <= r ) :: thesis: ( ex r being Real st

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

f . c <= r implies f | Y is bounded_above )

f . c <= r ; :: thesis: f | Y is bounded_above

reconsider r1 = r + 1 as Real ;

take r1 ; :: according to SEQ_2:def 1 :: thesis: for b_{1} being object holds

( not b_{1} in dom (f | Y) or not r1 <= (f | Y) . b_{1} )

let p be object ; :: thesis: ( not p in dom (f | Y) or not r1 <= (f | Y) . p )

assume A4: p in dom (f | Y) ; :: thesis: not r1 <= (f | Y) . p

then p in Y /\ (dom f) by RELAT_1:61;

then f . p <= r by A3;

then A5: (f | Y) . p <= r by A4, FUNCT_1:47;

r < r1 by XREAL_1:29;

hence not r1 <= (f | Y) . p by A5, XXREAL_0:2; :: thesis: verum

( f | Y is bounded_above iff ex r being Real st

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

f . c <= r )

let f be real-valued Function; :: thesis: ( f | Y is bounded_above iff ex r being Real st

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

f . c <= r )

thus ( f | Y is bounded_above implies ex r being Real st

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

f . c <= r ) :: thesis: ( ex r being Real st

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

f . c <= r implies f | Y is bounded_above )

proof

given r being Real such that A3:
for c being object st c in Y /\ (dom f) holds
given r being Real such that A1:
for p being object st p in dom (f | Y) holds

(f | Y) . p < r ; :: according to SEQ_2:def 1 :: thesis: ex r being Real st

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

f . c <= r

take 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 c in Y /\ (dom f) ; :: thesis: f . c <= r

then A2: c in dom (f | Y) by RELAT_1:61;

then (f | Y) . c < r by A1;

hence f . c <= r by A2, FUNCT_1:47; :: thesis: verum

end;(f | Y) . p < r ; :: according to SEQ_2:def 1 :: thesis: ex r being Real st

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

f . c <= r

take 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 c in Y /\ (dom f) ; :: thesis: f . c <= r

then A2: c in dom (f | Y) by RELAT_1:61;

then (f | Y) . c < r by A1;

hence f . c <= r by A2, FUNCT_1:47; :: thesis: verum

f . c <= r ; :: thesis: f | Y is bounded_above

reconsider r1 = r + 1 as Real ;

take r1 ; :: according to SEQ_2:def 1 :: thesis: for b

( not b

let p be object ; :: thesis: ( not p in dom (f | Y) or not r1 <= (f | Y) . p )

assume A4: p in dom (f | Y) ; :: thesis: not r1 <= (f | Y) . p

then p in Y /\ (dom f) by RELAT_1:61;

then f . p <= r by A3;

then A5: (f | Y) . p <= r by A4, FUNCT_1:47;

r < r1 by XREAL_1:29;

hence not r1 <= (f | Y) . p by A5, XXREAL_0:2; :: thesis: verum