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: f | X is bounded_below ;
A3: f | X is bounded_above by A1;
A4: rng f is bounded_below by A2, Th13;
rng f is bounded_above by A3, Th15;
hence rng f is bounded by A4; :: thesis: verum