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:58;
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:66;
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:8;
hence x is Element of (MonMaps (S,T)) by YELLOW_1:def 6; :: thesis: verum