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

now

let s be real number ; :: thesis: ( s in f .: the carrier of T implies s <= t )
assume s in f .: the carrier of T ; :: thesis: s <= t
then consider x being set such that
A2: ( x in the carrier of T & x in the carrier of T & s = f . x ) by FUNCT_2:115;
thus s <= t by A1, A2; :: thesis: verum

end;

hence sup f <= t by SEQ_4:62; :: thesis: verum