defpred S2[ object , object ] means ex p being FinSequence st
( len p >= 1 & p . 1 = $1 & p . (len p) = $2 & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) );
thus
ex S being Relation st
for x, y being object holds
( [x,y] in S iff ( x in field R & y in field R & S2[x,y] ) )
from RELAT_1:sch 1(); verum