let v1, w1 be Vertex of G1; :: thesis: ex W1 being Walk of G1 st W1 is_Walk_from v1,w1
E c= the_Edges_of G1 ;
then ( E c= G1 .edgesBetween (the_Vertices_of G1) & the_Vertices_of G1 c= the_Vertices_of G1 ) by GLIB_000:34;
then reconsider v2 = v1, w2 = w1 as Vertex of G2 by GLIB_000:def 37;
consider W2 being Walk of G2 such that
A2: W2 is_Walk_from v2,w2 by A1, GLIB_002:def 1;
reconsider W1 = W2 as Walk of G1 by GLIB_001:167;
take W1 = W1; :: thesis: W1 is_Walk_from v1,w1
thus W1 is_Walk_from v1,w1 by A2, GLIB_001:19; :: thesis: verum