let r be Real; :: thesis: for T being non empty TopSpace
for f being RealMap of T st ( for p being Point of T holds f . p <= r ) & ( for t being Real st ( for p being Point of T holds f . p <= t ) holds
r <= t ) holds
r = upper_bound f
let T be non empty TopSpace; :: thesis: for f being RealMap of T st ( for p being Point of T holds f . p <= r ) & ( for t being Real st ( for p being Point of T holds f . p <= t ) holds
r <= t ) holds
r = upper_bound f
let f be RealMap of T; :: thesis: ( ( for p being Point of T holds f . p <= r ) & ( for t being Real st ( for p being Point of T holds f . p <= t ) holds
r <= t ) implies r = upper_bound f )
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: r = upper_bound f

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

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

end;

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

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

end;

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