consider r being real number such that
W: for y being set st y in dom f holds
r < f . y by SEQ_2:def 2;
f | X is bounded_below

proof

take r ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in dom (f | X) or not (f | X) . b₁ <= r )
let y be set ; :: thesis: ( not y in dom (f | X) or not (f | X) . y <= r )
assume Z: y in dom (f | X) ; :: thesis: not (f | X) . y <= r
then y in dom f by RELAT_1:86;
then r < f . y by W;
hence not (f | X) . y <= r by Z, FUNCT_1:70; :: thesis: verum

end;

hence for b₁ being real-valued Function st b₁ = f | X holds
b₁ is bounded_below ; :: thesis: verum