let G be _Graph; :: thesis: for v1, v2, v3, v4 being Vertex of G st v1 <> v2 & v1 <> v3 & v2 <> v3 & v2 <> v4 & v3 <> v4 & v1,v2 are_adjacent & v2,v3 are_adjacent & v3,v4 are_adjacent holds
ex P being Path of G st
( len P = 7 & P .length() = 3 & P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
let v1, v2, v3, v4 be Vertex of G; :: thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 & v2 <> v4 & v3 <> v4 & v1,v2 are_adjacent & v2,v3 are_adjacent & v3,v4 are_adjacent implies ex P being Path of G st
( len P = 7 & P .length() = 3 & P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 ) )
assume that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3 and
A4: v2 <> v4 and
A5: v3 <> v4 and
A6: v1,v2 are_adjacent and
A7: v2,v3 are_adjacent and
A8: v3,v4 are_adjacent ; :: thesis: ex P being Path of G st
( len P = 7 & P .length() = 3 & P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
consider R being Path of G, e1, e2 being object such that
A9: R is open and
A10: len R = 5 and
R .length() = 2 and
A11: e1 Joins v1,v2,G and
A12: e2 Joins v2,v3,G and
A13: R .edges() = {e1,e2} and
A14: R .vertices() = {v1,v2,v3} and
A15: R . 1 = v1 and
A16: R . 3 = v2 and
A17: R . 5 = v3 by A1, A2, A3, A6, A7, Th46;
consider e3 being object such that
A18: e3 Joins v3,v4,G by A8;
A19: for n being odd Element of NAT st 1 < n & n <= len R holds
R . n <> v4

proof

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len R implies R . n <> v4 )
assume that
A20: 1 < n and
A21: n <= len R ; :: thesis: R . n <> v4

per cases ( n = 3 or n = 5 ) by A10, A20, A21, Th8, XXREAL_0:2;

suppose n = 3 ; :: thesis: R . n <> v4

hence R . n <> v4 by A4, A16; :: thesis: verum

end;

suppose n = 5 ; :: thesis: R . n <> v4

hence R . n <> v4 by A5, A17; :: thesis: verum

end;

end;

end;

A22: e2 <> e3 by A4, A18, A12;
set P = R .addEdge e3;
e1 <> e3 by A2, A3, A18, A11;
then not e3 in R .edges() by A13, A22, TARSKI:def 2;
then reconsider P = R .addEdge e3 as Path of G by A18, A9, A10, A17, A19, GLIB_001:150;
take P ; :: thesis: ( len P = 7 & P .length() = 3 & P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
A23: len P = 5 + 2 by A18, A10, A17, GLIB_001:64;
hence len P = 7 ; :: thesis: ( P .length() = 3 & P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
7 = (2 * (P .length())) + 1 by A23, GLIB_001:112;
hence P .length() = 3 ; :: thesis: ( P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
P .vertices() = {v1,v2,v3} \/ {v4} by A18, A10, A14, A17, GLIB_001:95;
hence P .vertices() = {v1,v2,v3,v4} by ENUMSET1:6; :: thesis: ( P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
1 in dom R by A10, FINSEQ_3:25;
hence P . 1 = v1 by A18, A10, A15, A17, GLIB_001:65; :: thesis: ( P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
3 in dom R by A10, FINSEQ_3:25;
hence P . 3 = v2 by A18, A10, A16, A17, GLIB_001:65; :: thesis: ( P . 5 = v3 & P . 7 = v4 )
5 in dom R by A10, FINSEQ_3:25;
hence P . 5 = v3 by A18, A10, A17, GLIB_001:65; :: thesis: P . 7 = v4
P .last() = v4 by A18, A10, A17, GLIB_001:63;
hence P . 7 = v4 by A23; :: thesis: verum