:: deftheorem defines are_joint_by LATTICE5:def 3 :
for X being non empty set
for f being non empty FinSequence of X
for x, y being object
for R1, R2 being Relation holds
( x,y are_joint_by f,R1,R2 iff ( f . 1 = x & f . (len f) = y & ( for i being Element of NAT st 1 <= i & i < len f holds
( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) ) );