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