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 = lower_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 = lower_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 = lower_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 = lower_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 = lower_bound f by A3, SEQ_4:44; :: thesis: verum