let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V
for W being Walk of G1 st W .edges() misses (G1 .loops()) \ (G2 .loops()) holds
W is Walk of G2
let V be set ; :: thesis: for G1 being addLoops of G2,V
for W being Walk of G1 st W .edges() misses (G1 .loops()) \ (G2 .loops()) holds
W is Walk of G2
let G1 be addLoops of G2,V; :: thesis: for W being Walk of G1 st W .edges() misses (G1 .loops()) \ (G2 .loops()) holds
W is Walk of G2
let W be Walk of G1; :: thesis: ( W .edges() misses (G1 .loops()) \ (G2 .loops()) implies W is Walk of G2 )
A1: G2 is Subgraph of G1 by GLIB_006:57;
assume A2: W .edges() misses (G1 .loops()) \ (G2 .loops()) ; :: thesis: W is Walk of G2

per cases ( V c= the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ;

suppose V c= the_Vertices_of G2 ; :: thesis: W is Walk of G2

then consider E being set , f being one-to-one Function such that
A3: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by Def5;

now :: thesis: for e being object st e in E holds
e in (G1 .loops()) \ (G2 .loops())

let e be object ; :: thesis: ( e in E implies e in (G1 .loops()) \ (G2 .loops()) )
assume A4: e in E ; :: thesis: e in (G1 .loops()) \ (G2 .loops())
then A5: ( (the_Source_of G1) . e = f . e & (the_Target_of G1) . e = f . e ) by A3, FUNCT_4:13;
A6: e in (the_Edges_of G2) \/ E by A4, XBOOLE_0:def 3;
then e Joins f . e,f . e,G1 by A3, A5, GLIB_000:def 13;
then A7: e in G1 .loops() by GLIB_009:def 2;
not e in G2 .loops() by A3, A4, A6, XBOOLE_0:5;
hence e in (G1 .loops()) \ (G2 .loops()) by A7, XBOOLE_0:def 5; :: thesis: verum

end;

then W .edges() misses E by A2, XBOOLE_1:63, TARSKI:def 3;
then A8: W .edges() c= the_Edges_of G2 by A3, XBOOLE_1:73;
W .vertices() c= the_Vertices_of G1 ;
then W .vertices() c= the_Vertices_of G2 by Th15;
hence W is Walk of G2 by A1, A8, GLIB_001:170; :: thesis: verum

end;

suppose not V c= the_Vertices_of G2 ; :: thesis: W is Walk of G2

then G1 == G2 by Def5;
hence W is Walk of G2 by GLIB_001:179; :: thesis: verum

end;

end;