let R1, R2 be Relation of [:the carrier of TS,(E ^omega ):]; :: thesis: ( ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS ) ) implies R1 = R2 )
assume that
A2:
for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS )
and
A3:
for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS )
; :: thesis: R1 = R2
now let s,
t be
Element of
[:the carrier of TS,(E ^omega ):];
:: thesis: ( [s,t] in R1 iff [s,t] in R2 )consider x,
u being
set such that B2:
(
x in the
carrier of
TS &
u in E ^omega &
s = [x,u] )
by ZFMISC_1:def 2;
reconsider x =
x as
Element of the
carrier of
TS by B2;
reconsider u =
u as
Element of
E ^omega by B2;
consider y,
v being
set such that B3:
(
y in the
carrier of
TS &
v in E ^omega &
t = [y,v] )
by ZFMISC_1:def 2;
reconsider y =
y as
Element of the
carrier of
TS by B3;
reconsider v =
v as
Element of
E ^omega by B3;
(
[s,t] in R1 iff
x,
u ==>. y,
v,
TS )
by A2, B2, B3;
hence
(
[s,t] in R1 iff
[s,t] in R2 )
by A3, B2, B3;
:: thesis: verum end;
hence
R1 = R2
by RELSET_1:def 3; :: thesis: verum