let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for W being Walk of G1 st W .vertices() misses V \ (the_Vertices_of G2) holds
W is Walk of G2
let V be set ; :: thesis: for G1 being addVertices of G2,V
for W being Walk of G1 st W .vertices() misses V \ (the_Vertices_of G2) holds
W is Walk of G2
let G1 be addVertices of G2,V; :: thesis: for W being Walk of G1 st W .vertices() misses V \ (the_Vertices_of G2) holds
W is Walk of G2
let W be Walk of G1; :: thesis: ( W .vertices() misses V \ (the_Vertices_of G2) implies W is Walk of G2 )
A1: G2 is Subgraph of G1 by Th61;
assume A2: W .vertices() misses V \ (the_Vertices_of G2) ; :: thesis: W is Walk of G2
the_Vertices_of G1 = (the_Vertices_of G2) \/ V by Def10;
then A3: the_Vertices_of G1 = (the_Vertices_of G2) \/ (V \ (the_Vertices_of G2)) by XBOOLE_1:39;
A4: W .vertices() c= the_Vertices_of G2 by A2, A3, XBOOLE_1:73;
W .edges() c= the_Edges_of G1 ;
then W .edges() c= the_Edges_of G2 by Def10;
hence W is Walk of G2 by A1, A4, GLIB_001:170; :: thesis: verum