theorem Th54: :: GRAPH_3:54

for X being set
for G being finite Graph
for v being Vertex of G
for p being Element of X -PathSet v
for Y being finite set st Y = the carrier' of G & Degree (v,X) <> 0 holds
len p <= card Y