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 object 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 object holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS )

now :: thesis: for x1, x2, y1, y2 being object holds
( ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) & ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS ) )

let x1, x2, y1, y2 be object ; :: 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];
A2: ( 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;
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 A3: x1,x2 ==>. y1,y2,TS ; :: thesis: [[x1,x2],[y1,y2]] in R
then y1 in TS by Th20;
then A4: y1 in the carrier of TS ;
x1 in TS by A3, Th20;
then A5: x1 in the carrier of TS ;
y2 in E ^omega by A3;
then A6: [y1,y2] in [: the carrier of TS,(E ^omega):] by A4, ZFMISC_1:def 2;
x2 in E ^omega by A3;
then [x1,x2] in [: the carrier of TS,(E ^omega):] by A5, ZFMISC_1:def 2;
hence [[x1,x2],[y1,y2]] in R by A1, A3, A6; :: thesis: verum

end;

assume A7: [[x1,x2],[y1,y2]] in R ; :: thesis: x1,x2 ==>. y1,y2,TS
then ( [x1,x2] in dom R & [y1,y2] in rng R ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
then consider x19, x29, y19, y29 being object such that
A8: [x19,x29] = [x1,x2] and
A9: [y19,y29] = [y1,y2] and
A10: x19,x29 ==>. y19,y29,TS by A1, A7, A2;
A11: y1 = y19 by A9, XTUPLE_0:1;
( x1 = x19 & x2 = x29 ) by A8, XTUPLE_0:1;
hence x1,x2 ==>. y1,y2,TS by A9, A10, A11, XTUPLE_0:1; :: thesis: verum

end;

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