A1: (f | X) .: the carrier of (T | X) is bounded_above by MEASURE6:def 15;
(f | X) .: X = f .: X by RELAT_1:162;
hence f .: X is bounded_above by A1, PRE_TOPC:29; :: thesis: verum