defpred S₁[ Element of E ^omega , Element of E ^omega ] means $1 ==>. $2,S;
consider R being Relation of (E ^omega) such that
A1: for s, t being Element of E ^omega holds
( [s,t] in R iff S₁[s,t] ) from RELSET_1:sch 2();
take R ; :: thesis: for s, t being Element of E ^omega holds
( [s,t] in R iff s ==>. t,S )
thus for s, t being Element of E ^omega holds
( [s,t] in R iff s ==>. t,S ) by A1; :: thesis: verum