let G2 be _Graph; for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for W being Walk of G1 st ( e in W .edges() implies e in the_Edges_of G2 ) holds
W is Walk of G2
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2
for W being Walk of G1 st ( e in W .edges() implies e in the_Edges_of G2 ) holds
W is Walk of G2
let e be object ; for G1 being addEdge of G2,v1,e,v2
for W being Walk of G1 st ( e in W .edges() implies e in the_Edges_of G2 ) holds
W is Walk of G2
let G1 be addEdge of G2,v1,e,v2; for W being Walk of G1 st ( e in W .edges() implies e in the_Edges_of G2 ) holds
W is Walk of G2
let W be Walk of G1; ( ( e in W .edges() implies e in the_Edges_of G2 ) implies W is Walk of G2 )
assume
( e in W .edges() implies e in the_Edges_of G2 )
; W is Walk of G2