defpred S₁[ object ] means ex f being Function of S,T st
( $1 = f & f is continuous );
consider X being set such that
A1: for a being object 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)) by A1;
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:8;
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