theorem Th44: :: GLENUM00:44

for G being _Graph
for S being non empty Subset of (G .allSG())
for G9 being GraphUnion of S st (SubgraphRel G) |_2 S is being_linear-order holds
for W being Walk of G9 ex H being Element of S st W is Walk of H