let T be non empty TopSpace; :: thesis: for f being bounded_above RealMap of T
for p being Point of T holds f . p <= upper_bound f
let f be bounded_above RealMap of T; :: thesis: for p being Point of T holds f . p <= upper_bound f
set fc = f .: the carrier of T;
let p be Point of T; :: thesis: f . p <= upper_bound f
( f .: the carrier of T is bounded_above & f . p in f .: the carrier of T ) by FUNCT_2:35, MEASURE6:def 11;
hence f . p <= upper_bound f by SEQ_4:def 1; :: thesis: verum