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 len W1 <= len W2 ; :: thesis: W1 .length() <= W2 .length()
then (2 * (W1 .length())) + 1 <= len W2 by GLIB_001:112;
then (2 * (W1 .length())) + 1 <= (2 * (W2 .length())) + 1 by GLIB_001:112;
then 2 * (W1 .length()) <= 2 * (W2 .length()) by XREAL_1:6;
then (2 * (W1 .length())) / 2 <= (2 * (W2 .length())) / 2 by XREAL_1:72;
hence W1 .length() <= W2 .length() ; :: thesis: verum

end;

assume W1 .length() <= W2 .length() ; :: thesis: len W1 <= len W2
then 2 * (W1 .length()) <= 2 * (W2 .length()) by XREAL_1:64;
then (2 * (W1 .length())) + 1 <= (2 * (W2 .length())) + 1 by XREAL_1:6;
then len W1 <= (2 * (W2 .length())) + 1 by GLIB_001:112;
hence len W1 <= len W2 by GLIB_001:112; :: thesis: verum