let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2 holds W2 is Walk of G1
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2 holds W2 is Walk of G1
let G1 be reverseEdgeDirections of G2,E; :: thesis: for W2 being Walk of G2 holds W2 is Walk of G1
let W2 be Walk of G2; :: thesis: W2 is Walk of G1

per cases ( E c= the_Edges_of G2 or not E c= the_Edges_of G2 ) ;

suppose E c= the_Edges_of G2 ; :: thesis: W2 is Walk of G1

W2 is FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G2) by Th4;
then A1: W2 is FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1) by Th4;
W2 . 1 in the_Vertices_of G2 by GLIB_001:def 3;
then A2: W2 . 1 in the_Vertices_of G1 by Th4;
for n being odd Element of NAT st n < len W2 holds
W2 . (n + 1) Joins W2 . n,W2 . (n + 2),G1 by Th9, GLIB_001:def 3;
hence W2 is Walk of G1 by A1, A2, GLIB_001:def 3; :: thesis: verum

end;

suppose not E c= the_Edges_of G2 ; :: thesis: W2 is Walk of G1

then G1 == G2 by Def1;
hence W2 is Walk of G1 by GLIB_001:179; :: thesis: verum

end;

end;