let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for W1 being Walk of G1 holds W1 is Walk of G2
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for W1 being Walk of G1 holds W1 is Walk of G2
let G1 be reverseEdgeDirections of G2,E; :: thesis: for W1 being Walk of G1 holds W1 is Walk of G2
let W1 be Walk of G1; :: thesis: W1 is Walk of G2
reconsider G3 = G2 as reverseEdgeDirections of G1,E by Th3;
W1 is Walk of G3 by Th14;
hence W1 is Walk of G2 ; :: thesis: verum