:: deftheorem Def11 defines -PathSet GRAPH_3:def 11 :
for G being finite Graph
for v being Vertex of G
for X being set st Degree (v,X) <> 0 holds
X -PathSet v = { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;