theorem :: INTEGRA2:5

for X, Y being non empty set
for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds
(f | Y) | Y is bounded_above