let G1 be _Graph; :: thesis: for E being set
for G2 being removeEdges of G1,E
for W1 being Walk of G1 st W1 .edges() misses E holds
W1 is Walk of G2
let E be set ; :: thesis: for G2 being removeEdges of G1,E
for W1 being Walk of G1 st W1 .edges() misses E holds
W1 is Walk of G2
let G2 be removeEdges of G1,E; :: thesis: for W1 being Walk of G1 st W1 .edges() misses E holds
W1 is Walk of G2
let W1 be Walk of G1; :: thesis: ( W1 .edges() misses E implies W1 is Walk of G2 )
assume A1: W1 .edges() misses E ; :: thesis: W1 is Walk of G2
A2: ( W1 .edges() c= the_Edges_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) by GLIB_000:53;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;
then W1 .vertices() c= the_Vertices_of G2 ;
hence W1 is Walk of G2 by A1, A2, XBOOLE_1:86, GLIB_001:170; :: thesis: verum