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

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

assume len W1 = len W2 ; :: thesis: W1 .length() = W2 .length()
then (2 * (W1 .length() )) + 1 = len W2 by Def15
.= (2 * (W2 .length() )) + 1 by Def15 ;
hence W1 .length() = W2 .length() ; :: thesis: verum

end;

assume W1 .length() = W2 .length() ; :: thesis: len W1 = len W2
hence len W1 = (2 * (W2 .length() )) + 1 by Def15
.= len W2 by Def15 ;
:: thesis: verum