A1: dom f = X by FUNCT_2:def 1;
thus ( f is bounded_below implies f .: X is bounded_below ) :: thesis: ( f .: X is bounded_below implies f is bounded_below )

proof

given r being real number such that A2: for y being set st y in dom f holds
r < f . y ; :: according to SEQ_2:def 2 :: thesis: f .: X is bounded_below
take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of f .: X
let s be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not s in f .: X or r <= s )
assume s in f .: X ; :: thesis: r <= s
then ex x being set st
( x in X & x in X & s = f . x ) by FUNCT_2:115;
hence r <= s by A1, A2; :: thesis: verum

end;

given p being real number such that A3: p is LowerBound of f .: X ; :: according to XXREAL_2:def 9 :: thesis: f is bounded_below
take p - 1 ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in proj1 f or not f . b₁ <= p - 1 )
let y be set ; :: thesis: ( not y in proj1 f or not f . y <= p - 1 )
assume y in dom f ; :: thesis: not f . y <= p - 1
then f . y in rng f by FUNCT_1:12;
then f . y in f .: X by RELSET_1:38;
then A4: p <= f . y by A3, XXREAL_2:def 2;
f . y < (f . y) + 1 by XREAL_1:31;
then p < (f . y) + 1 by A4, XXREAL_0:2;
hence not f . y <= p - 1 by XREAL_1:21; :: thesis: verum