defpred S1[ object ] means $1 is directed-sups-preserving Function of S,T;
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) & S1[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: ( SX is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of SX iff x is directed-sups-preserving Function of S,T ) ) )
thus SX is full SubRelStr of T |^ the carrier of S ; :: thesis: for x being set holds
( x in the carrier of SX iff x is directed-sups-preserving Function of S,T )
let f be set ; :: thesis: ( f in the carrier of SX iff f is directed-sups-preserving Function of S,T )
thus ( f in the carrier of SX implies f is directed-sups-preserving Function of S,T ) :: thesis: ( f is directed-sups-preserving Function of S,T implies f in the carrier of SX )
proof
assume f in the carrier of SX ; :: thesis: f is directed-sups-preserving Function of S,T
then f in X by YELLOW_0:def 15;
hence f is directed-sups-preserving Function of S,T by A1; :: thesis: verum
end;
assume A2: f is directed-sups-preserving Function of S,T ; :: thesis: f in the carrier of SX
then f is Element of (T |^ the carrier of S) by WAYBEL24:19;
then f in X by A1, A2;
hence f in the carrier of SX by YELLOW_0:def 15; :: thesis: verum