let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 holds
( len W1 = len W2 iff W1 .length() = W2 .length() )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 holds
( len W1 = len W2 iff W1 .length() = W2 .length() )
let W2 be Walk of G2; :: thesis: ( len W1 = len W2 iff W1 .length() = W2 .length() )

hereby :: thesis: ( W1 .length() = W2 .length() implies len W1 = len W2 )

assume A1: len W1 = len W2 ; :: thesis: W1 .length() = W2 .length()
(2 * (W1 .length())) + 1 = len W1 by GLIB_001:112
.= (2 * (W2 .length())) + 1 by A1, GLIB_001:112 ;
hence W1 .length() = W2 .length() ; :: thesis: verum

end;

assume A2: W1 .length() = W2 .length() ; :: thesis: len W1 = len W2
thus len W1 = (2 * (W1 .length())) + 1 by GLIB_001:112
.= len W2 by A2, GLIB_001:112 ; :: thesis: verum