let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let G2 be reverseEdgeDirections of G1,E; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let W2 be Walk of G2; :: thesis: ( W1 = W2 implies ( W1 is minlength iff W2 is minlength ) )
assume A1: W1 = W2 ; :: thesis: ( W1 is minlength iff W2 is minlength )
hence ( W1 is minlength implies W2 is minlength ) by Lm3; :: thesis: ( W2 is minlength implies W1 is minlength )
G1 is reverseEdgeDirections of G2,E by GLIB_007:3;
hence ( W2 is minlength implies W1 is minlength ) by A1, Lm3; :: thesis: verum