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

now

let s, t be Element of E ^omega ; :: thesis: ( [s,t] in R1 iff [s,t] in R2 )
( [s,t] in R1 iff s ==>. t,S ) by A2;
hence ( [s,t] in R1 iff [s,t] in R2 ) by A3; :: thesis: verum

end;

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