let G1 be _Graph; :: thesis: for W being Walk of G1

for e being set

for G2 being removeEdge of G1,e st not e in W .edges() holds

W is Walk of G2

let W be Walk of G1; :: thesis: for e being set

for G2 being removeEdge of G1,e st not e in W .edges() holds

W is Walk of G2

let e be set ; :: thesis: for G2 being removeEdge of G1,e st not e in W .edges() holds

W is Walk of G2

let G2 be removeEdge of G1,e; :: thesis: ( not e in W .edges() implies W is Walk of G2 )

A1: the_Edges_of G2 = (the_Edges_of G1) \ {e} by GLIB_000:53;

assume A2: not e in W .edges() ; :: thesis: W is Walk of G2

the_Vertices_of G2 = the_Vertices_of G1 by GLIB_000:53;

then W .vertices() c= the_Vertices_of G2 ;

hence W is Walk of G2 by A4, Th168; :: thesis: verum

for e being set

for G2 being removeEdge of G1,e st not e in W .edges() holds

W is Walk of G2

let W be Walk of G1; :: thesis: for e being set

for G2 being removeEdge of G1,e st not e in W .edges() holds

W is Walk of G2

let e be set ; :: thesis: for G2 being removeEdge of G1,e st not e in W .edges() holds

W is Walk of G2

let G2 be removeEdge of G1,e; :: thesis: ( not e in W .edges() implies W is Walk of G2 )

A1: the_Edges_of G2 = (the_Edges_of G1) \ {e} by GLIB_000:53;

assume A2: not e in W .edges() ; :: thesis: W is Walk of G2

now :: thesis: for x being object st x in W .edges() holds

x in the_Edges_of G2

then A4:
W .edges() c= the_Edges_of G2
by TARSKI:def 3;x in the_Edges_of G2

let x be object ; :: thesis: ( x in W .edges() implies x in the_Edges_of G2 )

assume A3: x in W .edges() ; :: thesis: x in the_Edges_of G2

then not x in {e} by A2, TARSKI:def 1;

hence x in the_Edges_of G2 by A1, A3, XBOOLE_0:def 5; :: thesis: verum

end;assume A3: x in W .edges() ; :: thesis: x in the_Edges_of G2

then not x in {e} by A2, TARSKI:def 1;

hence x in the_Edges_of G2 by A1, A3, XBOOLE_0:def 5; :: thesis: verum

the_Vertices_of G2 = the_Vertices_of G1 by GLIB_000:53;

then W .vertices() c= the_Vertices_of G2 ;

hence W is Walk of G2 by A4, Th168; :: thesis: verum