let G be _Graph; 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 ; ( 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
; 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; ( W .vertices() = {a,b} implies ex e being set st e Joins a,b,G )
assume A2:
W .vertices() = {a,b}
; ex e being set st e Joins a,b,G
A3:
W .first() in W .vertices()
by GLIB_001:88;
A4:
now 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,Glet x be
set ;
( 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
;
for y being set st y in {a,b} \ {x} holds
ex e being set st e Joins x,y,GA6:
(
x = a or
x = b )
by A2, A3, A5, TARSKI:def 2;
A7:
x in {x}
by TARSKI:def 1;
let y be
set ;
( y in {a,b} \ {x} implies ex e being set st e Joins x,y,G )assume A8:
y in {a,b} \ {x}
;
ex e being set st e Joins x,y,GA9:
(
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;
verum end;