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
now :: thesis: for x being object st x in W .edges() holds
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;
then A4: W .edges() c= the_Edges_of G2 by TARSKI:def 3;
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