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
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 ;
suppose n = 3 ; :: thesis: R . n <> v4
hence R . n <> v4 by ; :: thesis: verum
end;
suppose n = 5 ; :: thesis: R . n <> v4
hence R . n <> v4 by ; :: 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 ;
then reconsider P = R .addEdge e3 as Path of G by ;
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 ;
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 * ()) + 1 by ;
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 ;
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 ;
hence P . 1 = v1 by ; :: thesis: ( P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
3 in dom R by ;
hence P . 3 = v2 by ; :: thesis: ( P . 5 = v3 & P . 7 = v4 )
5 in dom R by ;
hence P . 5 = v3 by ; :: thesis: P . 7 = v4
P .last() = v4 by ;
hence P . 7 = v4 by A23; :: thesis: verum