theorem Th17: :: GRAPH_5:19

for V being set
for G being Graph
for pe being FinSequence of the carrier' of G holds
( vertices pe c= V iff for i being Nat st i in dom pe holds
vertices (pe /. i) c= V )