let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 holds
(len (maxPrefix (W1,W2))) + 2 <= len W1
let W1, W2 be Walk of G; :: thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 implies (len (maxPrefix (W1,W2))) + 2 <= len W1 )
assume ( W1 .first() = W2 .first() & not W1 c= W2 ) ; :: thesis: (len (maxPrefix (W1,W2))) + 2 <= len W1
then ( len (maxPrefix (W1,W2)) < len W1 & len (maxPrefix (W1,W2)) is odd Nat ) by Th8, Th22;
hence (len (maxPrefix (W1,W2))) + 2 <= len W1 by CHORD:4; :: thesis: verum