theorem Th22: :: PARTIT1:22

for Y being non empty set
for R1, R2 being Equivalence_Relation of Y
for f being FinSequence of Y
for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2