let R1, R2 be Relation of (E ^omega); :: thesis: ( ( for s, t being Element of E ^omega holds

( [s,t] in R1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds

( [s,t] in R2 iff s ==>. t,S ) ) implies R1 = R2 )

assume that

A2: for s, t being Element of E ^omega holds

( [s,t] in R1 iff s ==>. t,S ) and

A3: for s, t being Element of E ^omega holds

( [s,t] in R2 iff s ==>. t,S ) ; :: thesis: R1 = R2

for s, t being Element of E ^omega holds

( [s,t] in R1 iff [s,t] in R2 ) by A2, A3;

hence R1 = R2 by RELSET_1:def 2; :: thesis: verum

( [s,t] in R1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds

( [s,t] in R2 iff s ==>. t,S ) ) implies R1 = R2 )

assume that

A2: for s, t being Element of E ^omega holds

( [s,t] in R1 iff s ==>. t,S ) and

A3: for s, t being Element of E ^omega holds

( [s,t] in R2 iff s ==>. t,S ) ; :: thesis: R1 = R2

for s, t being Element of E ^omega holds

( [s,t] in R1 iff [s,t] in R2 ) by A2, A3;

hence R1 = R2 by RELSET_1:def 2; :: thesis: verum