let X, Y be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds
(f | Y) | Y is bounded_below
let f be PartFunc of X,REAL ; :: thesis: ( f | X is bounded_below & Y c= X implies (f | Y) | Y is bounded_below )
assume A1: f | X is bounded_below ; :: thesis: ( not Y c= X or (f | Y) | Y is bounded_below )
assume A2: Y c= X ; :: thesis: (f | Y) | Y is bounded_below
consider a being real number such that
A3: for x being set st x in X /\ (dom f) holds
f . x >= a by A1, RFUNCT_1:88;
for x being set st x in Y /\ (dom (f | Y)) holds
(f | Y) . x >= a

proof

let x be set ; :: thesis: ( x in Y /\ (dom (f | Y)) implies (f | Y) . x >= a )
assume x in Y /\ (dom (f | Y)) ; :: thesis: (f | Y) . x >= a
then A4: x in dom (f | Y) by XBOOLE_0:def 4;
then A5: x in (dom f) /\ Y by RELAT_1:90;
(dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26;
then a <= f . x by A3, A5;
hence (f | Y) . x >= a by A4, FUNCT_1:70; :: thesis: verum

end;

hence (f | Y) | Y is bounded_below by RFUNCT_1:88; :: thesis: verum