:: deftheorem Def3 defines Path_Rel OSALG_4:def 3 :
for R being non empty Poset
for b₂ being Equivalence_Relation of the carrier of R holds
( b₂ = Path_Rel R iff for x, y being object holds
( [x,y] in b₂ iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) );