set c = the carrier of T;
reconsider f = the carrier of T --> 0 as RealMap of T ;
take f ; :: thesis: f is bounded
( dom f = the carrier of T & rng f = {0 } ) by FUNCOP_1:14, FUNCT_2:def 1;
hence f .: the carrier of T is bounded_above by RELAT_1:146; :: according to SEQ_2:def 8,MEASURE6:def 15 :: thesis: f is bounded_below
thus f .: the carrier of T is bounded_below ; :: according to MEASURE6:def 14 :: thesis: verum