theorem :: INTEGRA1:15

for X being non empty set
for f being PartFunc of X,REAL st f | X is bounded holds
rng f is real-bounded by Th11, Th9;