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,PSCOMP_1:def 12 :: thesis: f is bounded_below
thus f .: the carrier of T is bounded_below ; :: according to PSCOMP_1:def 11 :: thesis: verum