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

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;

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

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 = {}

then A4:
the_Edges_of H = G .edgesBetween ((the_Vertices_of G) \ S)
by GLIB_000:def 37;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 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

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

then A8:
W .vertices() c= the_Vertices_of H
;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;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

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