:: deftheorem defines is_path_of SGRAPH1:def 9 :
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of g
for p being FinSequence of the carrier of g holds
( p is_path_of v1,v2 iff ( p . 1 = v1 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of NAT st 1 <= i & i < len p & i < j & j < len p holds
( p . i <> p . j & {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) ) );