set X = MonFuncs (S,T);
MonFuncs (S,T) c= Funcs ( the carrier of S, the carrier of T) by ORDERS_3:11;
then reconsider X = MonFuncs (S,T) as Subset of (T |^ the carrier of S) by Th28;
take SX = subrelstr X; :: thesis: for f being Function of S,T holds
( f in the carrier of SX iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
let f be Function of S,T; :: thesis: ( f in the carrier of SX iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )

hereby :: thesis: ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone implies f in the carrier of SX )

assume f in the carrier of SX ; :: thesis: ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone )
then f in X by YELLOW_0:def 15;
then ex f9 being Function of S,T st
( f9 = f & f9 in Funcs ( the carrier of S, the carrier of T) & f9 is monotone ) by ORDERS_3:def 6;
hence ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ; :: thesis: verum

end;

assume ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ; :: thesis: f in the carrier of SX
then f in X by ORDERS_3:def 6;
hence f in the carrier of SX by YELLOW_0:def 15; :: thesis: verum