let G be non-multi _Graph; :: thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds
W1 . ((len (maxPrefix W1,W2)) + 2) <> W2 . ((len (maxPrefix W1,W2)) + 2)
let W1, W2 be Walk of G; :: thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 implies W1 . ((len (maxPrefix W1,W2)) + 2) <> W2 . ((len (maxPrefix W1,W2)) + 2) )
assume that
A1: W1 .first() = W2 .first() and
A2: not W1 c= W2 and
A3: not W2 c= W1 and
A4: W1 . ((len (maxPrefix W1,W2)) + 2) = W2 . ((len (maxPrefix W1,W2)) + 2) ; :: thesis: contradiction
set dI = len (maxPrefix W1,W2);
A5: not len (maxPrefix W1,W2) is even by A1, Th21;
A6: W1 . ((len (maxPrefix W1,W2)) + 1) <> W2 . ((len (maxPrefix W1,W2)) + 1) by A2, A3, Th9;
A7: W1 . (len (maxPrefix W1,W2)) = W2 . (len (maxPrefix W1,W2)) by Th7;
A8: len (maxPrefix W1,W2) < len W1 by A2, Th8;
A9: len (maxPrefix W1,W2) < len W2 by A3, Th8;
A10: W1 . ((len (maxPrefix W1,W2)) + 1) Joins W1 . (len (maxPrefix W1,W2)),W1 . ((len (maxPrefix W1,W2)) + 2),G by A5, A8, GLIB_001:def 3;
W2 . ((len (maxPrefix W1,W2)) + 1) Joins W2 . (len (maxPrefix W1,W2)),W2 . ((len (maxPrefix W1,W2)) + 2),G by A5, A9, GLIB_001:def 3;
hence contradiction by A4, A6, A7, A10, GLIB_000:def 22; :: thesis: verum