let G be _Graph; :: thesis: for S being Subset of ()
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 (); :: 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 () \ S = {} end;
then A4: the_Edges_of H = G .edgesBetween (() \ S) by GLIB_000:def 37;
A5: W .edges() c= G .edgesBetween () by GLIB_001:109;
A6: the_Vertices_of H = () \ S by ;
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:
ex n being odd Element of NAT st
( n <= len W & W . n = x ) by ;
then not x in S by A1;
hence x in the_Vertices_of H by ; :: thesis: verum
end;
then A8: W .vertices() c= the_Vertices_of H ;
then G .edgesBetween () c= G .edgesBetween () by GLIB_000:36;
then W .edges() c= G .edgesBetween () by A5;
hence W is Walk of H by ; :: thesis: verum