let X be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded holds
rng f is bounded
let f be PartFunc of X,REAL ; :: thesis: ( f | X is bounded implies rng f is bounded )
assume A1: f | X is bounded ; :: thesis: rng f is bounded
then A2: rng f is bounded_above by Th15;
rng f is bounded_below by A1, Th13;
hence rng f is bounded by A2; :: thesis: verum