let T be non empty TopSpace; :: thesis: for f being bounded_above RealMap of T
for t being Real st ( for p being Point of T holds f . p <= t ) holds
upper_bound f <= t
let f be bounded_above RealMap of T; :: thesis: for t being Real st ( for p being Point of T holds f . p <= t ) holds
upper_bound f <= t
set c = the carrier of T;
set fc = f .: the carrier of T;
let t be Real; :: thesis: ( ( for p being Point of T holds f . p <= t ) implies upper_bound f <= t )
assume A1: for p being Point of T holds f . p <= t ; :: thesis: upper_bound f <= t

now :: thesis: for s being Real st s in f .: the carrier of T holds
s <= t

let s be Real; :: thesis: ( s in f .: the carrier of T implies s <= t )
assume s in f .: the carrier of T ; :: thesis: s <= t
then ex x being object st
( x in the carrier of T & x in the carrier of T & s = f . x ) by FUNCT_2:64;
hence s <= t by A1; :: thesis: verum

end;

hence upper_bound f <= t by SEQ_4:45; :: thesis: verum