defpred S₁[ Element of [:the carrier of TS,(E ^omega ):], Element of [:the carrier of TS,(E ^omega ):]] means ex x1, x2, y1, y2 being set st
( [x1,x2] = $1 & [y1,y2] = $2 & x1,x2 ==>. y1,y2,TS );
consider R being Relation of [:the carrier of TS,(E ^omega ):] such that
A1: for s, t being Element of [:the carrier of TS,(E ^omega ):] holds
( [s,t] in R iff S₁[s,t] ) from RELSET_1:sch 2();
take R ; :: thesis: for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS )

now

let x1, x2, y1, y2 be set ; :: thesis: ( ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) & ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS ) )
set s = [x1,x2];
set t = [y1,y2];
thus ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) :: thesis: ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS )

proof

assume A2: x1,x2 ==>. y1,y2,TS ; :: thesis: [[x1,x2],[y1,y2]] in R
then A3: ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega ) by ThDir10;
then ( x1 in the carrier of TS & y1 in the carrier of TS ) by STRUCT_0:def 5;
then ( [x1,x2] in [:the carrier of TS,(E ^omega ):] & [y1,y2] in [:the carrier of TS,(E ^omega ):] ) by A3, ZFMISC_1:def 2;
hence [[x1,x2],[y1,y2]] in R by A1, A2; :: thesis: verum

end;

assume A2: [[x1,x2],[y1,y2]] in R ; :: thesis: x1,x2 ==>. y1,y2,TS
A3: ( [x1,x2] in dom R & [y1,y2] in rng R ) by A2, RELAT_1:20;
( dom R c= [:the carrier of TS,(E ^omega ):] & rng R c= [:the carrier of TS,(E ^omega ):] ) by RELAT_1:def 18, RELAT_1:def 19;
then consider x1', x2', y1', y2' being set such that
A4: ( [x1',x2'] = [x1,x2] & [y1',y2'] = [y1,y2] & x1',x2' ==>. y1',y2',TS ) by A1, A2, A3;
( x1 = x1' & x2 = x2' & y1 = y1' & y2 = y2' ) by A4, ZFMISC_1:33;
hence x1,x2 ==>. y1,y2,TS by A4; :: thesis: verum

end;

hence for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS ) ; :: thesis: verum