let T be non empty 1-sorted ; :: thesis: for f being bounded RealMap of T holds lower_bound f <= upper_bound f
let f be bounded RealMap of T; :: thesis: lower_bound f <= upper_bound f
( f .: the carrier of T is bounded_below & f .: the carrier of T is bounded_above ) by MEASURE6:def 10, MEASURE6:def 11;
hence lower_bound f <= upper_bound f by SEQ_4:11; :: thesis: verum