let G2 be _Graph; :: thesis: for G1 being reverseEdgeDirections of G2
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is directed iff W2 .reverse() is directed )
let G1 be reverseEdgeDirections of G2; :: thesis: for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is directed iff W2 .reverse() is directed )
let W2 be Walk of G2; :: thesis: for W1 being Walk of G1 st W1 = W2 holds
( W1 is directed iff W2 .reverse() is directed )
let W1 be Walk of G1; :: thesis: ( W1 = W2 implies ( W1 is directed iff W2 .reverse() is directed ) )
assume A1: W1 = W2 ; :: thesis: ( W1 is directed iff W2 .reverse() is directed )
W2 .edges() c= the_Edges_of G2 ;
hence ( W1 is directed iff W2 .reverse() is directed ) by A1, Th16; :: thesis: verum