consider r being Real such that
A1: for y being object 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 b1 being object holds
( not b1 in dom (f | X) or not (f | X) . b1 <= r )
let y be object ; :: thesis: ( not y in dom (f | X) or not (f | X) . y <= r )
assume A2: y in dom (f | X) ; :: thesis: not (f | X) . y <= r
then y in dom f by RELAT_1:57;
then r < f . y by A1;
hence not (f | X) . y <= r by A2, FUNCT_1:47; :: thesis: verum
end;
hence for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_below ; :: thesis: verum