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

A3: now :: thesis:

let t be Real; :: thesis:
assume for s being Real st s in f .: the carrier of T holds
s <= t ; :: thesis:
then for s being Point of T holds f . s <= t by FUNCT_2:35;
hence r <= t by A2; :: thesis:

end;

let s be Real; :: thesis:
assume s in f .: the carrier of T ; :: thesis:
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 <= r by A1; :: thesis:

end;

hence r = upper_bound f by A3, SEQ_4:46; :: thesis: