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