let T be non empty TopSpace; :: thesis: for f being bounded_below RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s
let f be bounded_below RealMap of T; :: thesis: for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s
set c = the carrier of T;
set fc = f .: the carrier of T;
let s be Real; :: thesis: ( ( for t being Point of T holds f . t >= s ) implies lower_bound f >= s )
assume A1: for t being Point of T holds f . t >= s ; :: thesis: lower_bound f >= s

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

let p1 be Real; :: thesis: ( p1 in f .: the carrier of T implies p1 >= s )
assume p1 in f .: the carrier of T ; :: thesis: p1 >= s
then ex x being object st
( x in the carrier of T & x in the carrier of T & p1 = f . x ) by FUNCT_2:64;
hence p1 >= s by A1; :: thesis: verum

end;

hence lower_bound f >= s by SEQ_4:43; :: thesis: verum