rng (f | X) c= rng f by RELAT_1:70;
hence f | X is surreal-valued ; :: thesis: verum