defpred S₁[ set ] means ex f being Function of S,T st
( $1 = f & f is continuous );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in the carrier of (MonMaps S,T) & S₁[a] ) ) from XBOOLE_0:sch 1();
X c= the carrier of (MonMaps S,T)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in the carrier of (MonMaps S,T) )
assume a in X ; :: thesis: a in the carrier of (MonMaps S,T)
hence a in the carrier of (MonMaps S,T) by A1; :: thesis: verum

end;

then reconsider X = X as Subset of (MonMaps S,T) ;
take SX = subrelstr X; :: thesis: for f being Function of S,T holds
( f in the carrier of SX iff f is continuous )
let f be Function of S,T; :: thesis: ( f in the carrier of SX iff f is continuous )

hereby :: thesis: ( f is continuous implies f in the carrier of SX )

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

end;

assume A2: f is continuous ; :: thesis: f in the carrier of SX
f in Funcs the carrier of S,the carrier of T by FUNCT_2:11;
then f in the carrier of (MonMaps S,T) by A2, YELLOW_1:def 6;
then f in X by A1, A2;
hence f in the carrier of SX by YELLOW_0:def 15; :: thesis: verum