:: deftheorem defines MonMaps YELLOW_1:def 6 :
for S, T being RelStr
for b₃ being strict full SubRelStr of T |^ the carrier of S holds
( b₃ = MonMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b₃ iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) );