let Y be set ; :: thesis: for f being real-valued Function holds
( f | Y is bounded_above iff ex r being real number st
for c being set 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 number st
for c being set st c in Y /\ (dom f) holds
f . c <= r )
thus ( f | Y is bounded_above implies ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r ) :: thesis: ( ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r implies f | Y is bounded_above )

proof

given r being real number such that A1: for p being set st p in dom (f | Y) holds
(f | Y) . p < r ; :: according to SEQ_2:def 1 :: thesis: ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r
take 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 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;

given r being real number such that A3: for c being set st c in Y /\ (dom f) holds
f . c <= r ; :: thesis: f | Y is bounded_above
reconsider r1 = r + 1 as real number ;
take r1 ; :: according to SEQ_2:def 1 :: thesis: for b₁ being set holds
( not b₁ in proj1 (f | Y) or not r1 <= K250((f | Y),b₁) )
let p be set ; :: thesis: ( not p in proj1 (f | Y) or not r1 <= K250((f | Y),p) )
assume A4: p in dom (f | Y) ; :: thesis: not r1 <= K250((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 <= K250((f | Y),p) by A5, XXREAL_0:2; :: thesis: verum