let T be non empty TopSpace; :: thesis: for f being V38() RealMap of T
for p being Point of T holds f . p >= inf f
let f be V38() RealMap of T; :: thesis: for p being Point of T holds f . p >= inf f
set fc = f .: the carrier of T;
A1: f .: the carrier of T is bounded_below by Def11;
set r = inf f;
let p be Point of T; :: thesis: f . p >= inf f
f . p in f .: the carrier of T by FUNCT_2:43;
hence f . p >= inf f by A1, SEQ_4:def 5; :: thesis: verum