theorem Th18: :: GRAPH_5:20

for V being set
for G being Graph
for pe being FinSequence of the carrier' of G st not vertices pe c= V holds
ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st
( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V )