let G be _Graph; :: thesis: for W being Walk of G holds W .length() = (W .reverse()) .length()
let W be Walk of G; :: thesis: W .length() = (W .reverse()) .length()
A1: len W = (2 * (W .length())) + 1 by GLIB_001:112;
len W = len (W .reverse()) by GLIB_001:21;
then ((2 * (W .length())) + 1) - 1 = ((2 * ((W .reverse()) .length())) + 1) - 1 by A1, GLIB_001:112;
hence W .length() = (W .reverse()) .length() ; :: thesis: verum