set c = the carrier of T;
reconsider f = the carrier of T --> 0 as RealMap of T ;
take f ; :: thesis: f is bounded
A1: dom f = the carrier of T by FUNCT_2:def 1;
rng f = {0 } by FUNCOP_1:14;
then f .: the carrier of T = {0 } by A1, RELAT_1:146;
then f .: the carrier of T is bounded ;
hence f .: the carrier of T is bounded_above ; :: 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