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