let r be real number ; :: 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 number 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 number 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 number 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 number st ( for p being Point of T holds f . p >= t ) holds
r >= t ; :: thesis: r = lower_bound f

A3: now

let t be real number ; :: thesis: ( ( for s being real number st s in f .: the carrier of T holds
s >= t ) implies r >= t )
assume for s being real number 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:43;
hence r >= t by A2; :: thesis: verum

end;

now

let s be real number ; :: 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 set st
( x in the carrier of T & x in the carrier of T & s = f . x ) by FUNCT_2:115;
hence s >= r by A1; :: thesis: verum

end;

hence r = lower_bound f by A3, SEQ_4:61; :: thesis: verum