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 natural odd number 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 natural odd number 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 natural odd number 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 natural odd number 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

now

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

end;

then A3: ( the_Vertices_of H = (the_Vertices_of G) \ S & the_Edges_of H = G .edgesBetween ((the_Vertices_of G) \ S) ) by GLIB_000:def 39;

now

let x be set ; :: thesis: ( x in W .vertices() implies x in the_Vertices_of H )
assume A4: x in W .vertices() ; :: thesis: x in the_Vertices_of H
consider n being odd Element of NAT such that
A5: ( n <= len W & W . n = x ) by A4, GLIB_001:88;
( x in the_Vertices_of G & not x in S ) by A1, A5, GLIB_001:8;
hence x in the_Vertices_of H by A3, XBOOLE_0:def 5; :: thesis: verum

end;

then A6: W .vertices() c= the_Vertices_of H by TARSKI:def 3;
A7: W .edges() c= G .edgesBetween (W .vertices() ) by GLIB_001:110;
G .edgesBetween (W .vertices() ) c= G .edgesBetween (the_Vertices_of H) by A6, GLIB_000:39;
then W .edges() c= G .edgesBetween (the_Vertices_of H) by A7, XBOOLE_1:1;
hence W is Walk of H by A3, A6, GLIB_001:171; :: thesis: verum