consider f being monotone Function of S,T;
f in Funcs the carrier of S,the carrier of T by FUNCT_2:11;
then f in the carrier of (MonMaps S,T) by YELLOW_1:def 6;
hence not MonMaps S,T is empty ; :: thesis: verum