theorem :: INTEGRA2:6

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