let G be _Graph; :: thesis: for S being Subset of (the_Vertices_of G)
for H being removeVertices of G,S
for W being Walk of G st ( for n being odd Nat st n <= len W holds
not W . n in S ) holds
W is Walk of H
let S be Subset of (the_Vertices_of G); :: thesis: for H being removeVertices of G,S
for W being Walk of G st ( for n being odd Nat st n <= len W holds
not W . n in S ) holds
W is Walk of H
let H be removeVertices of G,S; :: thesis: for W being Walk of G st ( for n being odd Nat st n <= len W holds
not W . n in S ) holds
W is Walk of H
let W be Walk of G; :: thesis: ( ( for n being odd Nat st n <= len W holds
not W . n in S ) implies W is Walk of H )
assume A1: for n being odd Nat st n <= len W holds
not W . n in S ; :: thesis: W is Walk of H

A2: now :: thesis: not (the_Vertices_of G) \ S = {}

assume (the_Vertices_of G) \ S = {} ; :: thesis: contradiction
then A3: the_Vertices_of G c= S by XBOOLE_1:37;
W .last() in the_Vertices_of G ;
hence contradiction by A1, A3; :: thesis: verum

end;

then A4: the_Edges_of H = G .edgesBetween ((the_Vertices_of G) \ S) by GLIB_000:def 37;
A5: W .edges() c= G .edgesBetween (W .vertices()) by GLIB_001:109;
A6: the_Vertices_of H = (the_Vertices_of G) \ S by A2, GLIB_000:def 37;

now :: thesis: for x being object st x in W .vertices() holds
x in the_Vertices_of H

let x be object ; :: thesis: ( x in W .vertices() implies x in the_Vertices_of H )
assume A7: x in W .vertices() ; :: thesis: x in the_Vertices_of H
ex n being odd Element of NAT st
( n <= len W & W . n = x ) by A7, GLIB_001:87;
then not x in S by A1;
hence x in the_Vertices_of H by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then A8: W .vertices() c= the_Vertices_of H ;
then G .edgesBetween (W .vertices()) c= G .edgesBetween (the_Vertices_of H) by GLIB_000:36;
then W .edges() c= G .edgesBetween (the_Vertices_of H) by A5;
hence W is Walk of H by A6, A4, A8, GLIB_001:170; :: thesis: verum