let T be non empty TopSpace; :: thesis: for X being non empty compact Subset of T
for f being continuous RealMap of T holds f .: X is bounded_below
let X be non empty compact Subset of T; :: thesis: for f being continuous RealMap of T holds f .: X is bounded_below
let f be continuous RealMap of T; :: thesis: f .: X is bounded_below
A1: (f | X) .: X = f .: X by RELAT_1:162;
(f | X) .: the carrier of (T | X) is bounded_below by PSCOMP_1:def 11;
hence f .: X is bounded_below by A1, PRE_TOPC:29; :: thesis: verum