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

proof

given r being real number such that G: for p being set st p in dom (f | Y) holds
r < (f | Y) . p ; :: according to SEQ_2:def 2 :: thesis: ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c
take r ; :: thesis: for c being set st c in Y /\ (dom f) holds
r <= f . c
let c be set ; :: thesis: ( c in Y /\ (dom f) implies r <= f . c )
assume c in Y /\ (dom f) ; :: thesis: r <= f . c
then Z: c in dom (f | Y) by RELAT_1:90;
then r < (f | Y) . c by G;
hence r <= f . c by Z, FUNCT_1:70; :: thesis: verum

end;

given r being real number such that G: for c being set st c in Y /\ (dom f) holds
r <= f . c ; :: thesis: f | Y is bounded_below
reconsider r1 = r - 1 as real number ;
A: r1 < r by XREAL_1:46;
take r1 ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in dom (f | Y) or not (f | Y) . b₁ <= r1 )
let p be set ; :: thesis: ( not p in dom (f | Y) or not (f | Y) . p <= r1 )
assume Z: p in dom (f | Y) ; :: thesis: not (f | Y) . p <= r1
then p in Y /\ (dom f) by RELAT_1:90;
then r <= f . p by G;
then r <= (f | Y) . p by Z, FUNCT_1:70;
hence not (f | Y) . p <= r1 by A, XXREAL_0:2; :: thesis: verum