set f = the monotone Function of S,T;
the monotone Function of S,T in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8;
hence not MonMaps (S,T) is empty by YELLOW_1:def 6; :: thesis: verum