let S be RelStr ; :: thesis: 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 )
let T be non empty reflexive RelStr ; :: thesis: for x being set holds
( x is Element of (MonMaps S,T) iff x is monotone Function of S,T )
let x be set ; :: thesis: ( x is Element of (MonMaps S,T) iff x is monotone Function of S,T )

hereby :: thesis: ( x is monotone Function of S,T implies x is Element of (MonMaps S,T) )

assume x is Element of (MonMaps S,T) ; :: thesis: x is monotone Function of S,T
then reconsider f = x as Element of (MonMaps S,T) ;
f is Element of (T |^ the carrier of S) by YELLOW_0:59;
then f in the carrier of (T |^ the carrier of S) ;
then f in Funcs the carrier of S,the carrier of T by YELLOW_1:28;
then reconsider f = f as Function of S,T by FUNCT_2:121;
f in the carrier of (MonMaps S,T) ;
hence x is monotone Function of S,T by YELLOW_1:def 6; :: thesis: verum

end;

assume x is monotone Function of S,T ; :: thesis: x is Element of (MonMaps S,T)
then reconsider f = x as monotone Function of S,T ;
f in Funcs the carrier of S,the carrier of T by FUNCT_2:11;
hence x is Element of (MonMaps S,T) by YELLOW_1:def 6; :: thesis: verum