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;

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

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 A2, A3, A5, TARSKI:def 2;

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 A8, TARSKI:def 2;

set k = W .find y;

A10: W . (W .find y) = y by A2, A8, GLIB_001:def 19;

then W .find y <> 1 by A5, A8, A7, XBOOLE_0:def 5;

then consider m being odd Nat such that

A11: m + 2 = W .find y by Th5;

A12: m < W .find y by A11, NAT_1:16;

W .find y <= len W by A2, A8, GLIB_001:def 19;

then A13: m < len W by A11, NAT_1:16, XXREAL_0:2;

A14: m in NAT by ORDINAL1:def 12;

then W . m in {a,b} by A2, A13, GLIB_001:87;

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 A11, A13, A14, GLIB_001:def 3;

hence ex e being set st e Joins x,y,G by A2, A8, A7, A6, A10, A12, A13, A15, A9, GLIB_001:def 19, XBOOLE_0:def 5; :: thesis: verum

end;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 A2, A3, A5, TARSKI:def 2;

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 A8, TARSKI:def 2;

set k = W .find y;

A10: W . (W .find y) = y by A2, A8, GLIB_001:def 19;

then W .find y <> 1 by A5, A8, A7, XBOOLE_0:def 5;

then consider m being odd Nat such that

A11: m + 2 = W .find y by Th5;

A12: m < W .find y by A11, NAT_1:16;

W .find y <= len W by A2, A8, GLIB_001:def 19;

then A13: m < len W by A11, NAT_1:16, XXREAL_0:2;

A14: m in NAT by ORDINAL1:def 12;

then W . m in {a,b} by A2, A13, GLIB_001:87;

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 A11, A13, A14, GLIB_001:def 3;

hence ex e being set st e Joins x,y,G by A2, A8, A7, A6, A10, A12, A13, A15, A9, GLIB_001:def 19, XBOOLE_0:def 5; :: thesis: verum

per cases
( W .first() = a or W .first() = b )
by A2, A3, TARSKI:def 2;

end;

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 A1, ZFMISC_1:17;

hence ex e being set st e Joins a,b,G by A4, A16; :: thesis: verum

end;then b in {a,b} \ {a} by A1, ZFMISC_1:17;

hence ex e being set st e Joins a,b,G by A4, A16; :: thesis: verum

suppose A17:
W .first() = b
; :: thesis: ex e being set st e Joins a,b,G

a in {a}
by TARSKI:def 1;

then a in {a,b} \ {b} by A1, ZFMISC_1:17;

then ex e being set st e Joins b,a,G by A4, A17;

hence ex e being set st e Joins a,b,G by GLIB_000:14; :: thesis: verum

end;then a in {a,b} \ {b} by A1, ZFMISC_1:17;

then ex e being set st e Joins b,a,G by A4, A17;

hence ex e being set st e Joins a,b,G by GLIB_000:14; :: thesis: verum