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

proof

given r being Real such that A6: for y being object st y in dom f holds
r > f . y ; :: according to SEQ_2:def 1 :: thesis: f .: X is bounded_above
take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of f .: X
let s be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not s in f .: X or s <= r )
assume s in f .: X ; :: thesis: s <= r
then ex x being object st
( x in X & x in X & s = f . x ) by FUNCT_2:64;
hence s <= r by A5, A6; :: thesis: verum

end;

given p being Real such that A7: p is UpperBound of f .: X ; :: according to XXREAL_2:def 10 :: thesis: f is bounded_above
take p + 1 ; :: according to SEQ_2:def 1 :: thesis: for b₁ being object holds
( not b₁ in dom f or not p + 1 <= f . b₁ )
let y be object ; :: thesis: ( not y in dom f or not p + 1 <= f . y )
assume y in dom f ; :: thesis: not p + 1 <= f . y
then f . y in rng f by FUNCT_1:3;
then f . y in f .: X by RELSET_1:22;
then p >= f . y by A7, XXREAL_2:def 1;
then A8: p + 1 >= (f . y) + 1 by XREAL_1:6;
f . y < (f . y) + 1 by XREAL_1:29;
hence not p + 1 <= f . y by A8, XXREAL_0:2; :: thesis: verum