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

proof

take r ; :: according to SEQ_2:def 1 :: thesis: for b₁ being set holds
( not b₁ in proj1 (f | X) or not r <= K250((f | X),b₁) )
let y be set ; :: thesis: ( not y in proj1 (f | X) or not r <= K250((f | X),y) )
assume A2: y in dom (f | X) ; :: thesis: not r <= K250((f | X),y)
then y in dom f by RELAT_1:57;
then f . y < r by A1;
hence not r <= K250((f | X),y) by A2, FUNCT_1:47; :: thesis: verum

end;

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