:: deftheorem defines [*] FINSEQ_1:def 16 :
for R, b₂ being Relation holds
( b₂ = R [*] iff for x, y being object holds
( [x,y] in b₂ iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) );