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()
len W = len (W .reverse()) by GLIB_001:21;
hence W .length() = (W .reverse()) .length() by GLIB_001:113; :: thesis: verum