defpred S_{1}[ 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_{1}[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

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

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