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 f | X is bounded_below ; :: thesis: ( not Y c= X or (f | Y) | Y is bounded_below )
then consider a being Real such that
A1: for x being object st x in X /\ (dom f) holds
f . x >= a by RFUNCT_1:71;
assume A2: Y c= X ; :: thesis: (f | Y) | Y is bounded_below
for x being object st x in Y /\ (dom (f | Y)) holds
(f | Y) . x >= a

proof

let x be object ; :: thesis: ( x in Y /\ (dom (f | Y)) implies (f | Y) . x >= a )
A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26;
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 x in (dom f) /\ Y by RELAT_1:61;
then a <= f . x by A1, A3;
hence (f | Y) . x >= a by A4, FUNCT_1:47; :: thesis: verum

end;

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