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_{1} being real-valued Function st b_{1} = f | X holds

b_{1} is bounded_below
; :: thesis: verum

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

hence
for b
take
r
; :: according to SEQ_2:def 2 :: thesis: for b_{1} being object holds

( not b_{1} in dom (f | X) or not (f | X) . b_{1} <= 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;( not b

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

b