defpred S1[ 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 S1[s,t] )
from RELSET_1:sch 2();
take
R
; for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS )
now 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 ;
( ( 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 )
( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS )proof
assume A3:
x1,
x2 ==>. y1,
y2,
TS
;
[[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;
verum
end; assume A7:
[[x1,x2],[y1,y2]] in R
;
x1,x2 ==>. y1,y2,TSthen
(
[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;
verum end;
hence
for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS )
; verum