theorem Th11: :: REWRITE1:11

for R being Relation
for a, b being object holds
( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )