A2: (f | X) .: the carrier of (T | X) is bounded_above by MEASURE6:def 11;
(f | X) .: X = f .: X by RELAT_1:129;
hence f .: X is bounded_above by A2, PRE_TOPC:8; :: thesis: verum