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