let T be non empty 1-sorted ; :: thesis: for f being bounded RealMap of T holds inf f <= sup f
let f be bounded RealMap of T; :: thesis: inf f <= sup f
( f .: the carrier of T is bounded_below & f .: the carrier of T is bounded_above ) by Def11, Def12;
then f .: the carrier of T is bounded ;
hence inf f <= sup f by SEQ_4:24; :: thesis: verum