theorem Th126: :: GLIBPRE1:123

for G1, G2 being _Graph
for G being GraphUnion of G1,G2
for W being Walk of G st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & W is not Walk of G1 holds
W is Walk of G2 by Lm4;