let G be _Graph; :: thesis: for a, b being set st a <> b holds
for W being Walk of G st W .vertices() = {a,b} holds
ex e being set st e Joins a,b,G

let a, b be set ; :: thesis: ( a <> b implies for W being Walk of G st W .vertices() = {a,b} holds
ex e being set st e Joins a,b,G )

assume A1: a <> b ; :: thesis: for W being Walk of G st W .vertices() = {a,b} holds
ex e being set st e Joins a,b,G

let W be Walk of G; :: thesis: ( W .vertices() = {a,b} implies ex e being set st e Joins a,b,G )
assume A2: W .vertices() = {a,b} ; :: thesis: ex e being set st e Joins a,b,G
A3: W .first() in W .vertices() by GLIB_001:88;
A4: now :: thesis: for x being set st W .first() = x holds
for y being set st y in {a,b} \ {x} holds
ex e being set st e Joins x,y,G
let x be set ; :: thesis: ( W .first() = x implies for y being set st y in {a,b} \ {x} holds
ex e being set st e Joins x,y,G )

assume A5: W .first() = x ; :: thesis: for y being set st y in {a,b} \ {x} holds
ex e being set st e Joins x,y,G

A6: ( x = a or x = b ) by ;
A7: x in {x} by TARSKI:def 1;
let y be set ; :: thesis: ( y in {a,b} \ {x} implies ex e being set st e Joins x,y,G )
assume A8: y in {a,b} \ {x} ; :: thesis: ex e being set st e Joins x,y,G
A9: ( y = a or y = b ) by ;
set k = W .find y;
A10: W . (W .find y) = y by ;
then W .find y <> 1 by ;
then consider m being odd Nat such that
A11: m + 2 = W .find y by Th5;
A12: m < W .find y by ;
W .find y <= len W by ;
then A13: m < len W by ;
A14: m in NAT by ORDINAL1:def 12;
then W . m in {a,b} by ;
then A15: ( W . m = a or W . m = b ) by TARSKI:def 2;
W . (m + 1) Joins W . m,W . (W .find y),G by ;
hence ex e being set st e Joins x,y,G by ; :: thesis: verum
end;
per cases ( W .first() = a or W .first() = b ) by ;
suppose A16: W .first() = a ; :: thesis: ex e being set st e Joins a,b,G
b in {b} by TARSKI:def 1;
then b in {a,b} \ {a} by ;
hence ex e being set st e Joins a,b,G by ; :: thesis: verum
end;
suppose A17: W .first() = b ; :: thesis: ex e being set st e Joins a,b,G
end;
end;