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 (T |^ the carrier of S) & S₁[a] ) ) from XBOOLE_0:sch 1();
X c= the carrier of (T |^ the carrier of S) by A1;
then reconsider X = X as Subset of (T |^ the carrier of S) ;
take SX = subrelstr X; :: thesis:
thus SX is full SubRelStr of T |^ the carrier of S ; :: thesis:
let f be set ; :: thesis:

assume f in the carrier of SX ; :: thesis:
then f in X by YELLOW_0:def 15;
then consider f9 being Function of S,T such that
A2: ( f9 = f & f9 is continuous ) by A1;
take f9 = f9; :: thesis:
thus ( f9 = f & f9 is continuous ) by A2; :: thesis:

end;