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:113;
len W = len (W .reverse() ) by GLIB_001:22;
then ((2 * (W .length() )) + 1) - 1 = ((2 * ((W .reverse() ) .length() )) + 1) - 1 by A1, GLIB_001:113;
hence W .length() = (W .reverse() ) .length() ; :: thesis: verum