theorem :: INTEGRA1:14

for X being non empty set
for f being PartFunc of X,REAL st rng f is bounded_above holds
f | X is bounded_above