theorem Th9: :: WAYBEL10:9

for S being RelStr
for T being non empty reflexive RelStr
for x being set holds
( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )