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 & v1 <> v3 & v2 <> v3 & v2 <> v4 & v3 <> v4 ) and
A2: ( v1,v2 are_adjacent & v2,v3 are_adjacent & 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 e3 being set such that
A3: e3 Joins v3,v4,G by A2, Def3;
consider R being Path of G, e1, e2 being set such that
A4: not R is closed and
A5: ( len R = 5 & R .length() = 2 ) and
A6: ( e1 Joins v1,v2,G & e2 Joins v2,v3,G & R .edges() = {e1,e2} ) and
A7: R .vertices() = {v1,v2,v3} and
A8: ( R . 1 = v1 & R . 3 = v2 & R . 5 = v3 ) by A1, A2, Th47;
A9: e1 <> e3 by A1, A3, A6, GLIB_000:18;
e2 <> e3 by A1, A3, A6, GLIB_000:18;
then A10: not e3 in R .edges() by A6, A9, TARSKI:def 2;
A11: 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
A12: 1 < n and
A13: n <= len R ; :: thesis: R . n <> v4

per cases ( n = 3 or n = 5 ) by A5, A12, A13, Th8, XXREAL_0:2;

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

hence R . n <> v4 by A1, A8; :: thesis: verum

end;

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

hence R . n <> v4 by A1, A8; :: thesis: verum

end;

end;

end;

set P = R .addEdge e3;
reconsider P = R .addEdge e3 as Path of G by A3, A4, A5, A8, A10, A11, GLIB_001:151;
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 )
A14: len P = 5 + 2 by A3, A5, A8, GLIB_001:65;
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 A14, GLIB_001:113;
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 A3, A5, A7, A8, GLIB_001:96;
hence P .vertices() = {v1,v2,v3,v4} by ENUMSET1:46; :: thesis: ( P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
1 in dom R by A5, FINSEQ_3:27;
hence P . 1 = v1 by A3, A5, A8, GLIB_001:66; :: thesis: ( P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )
3 in dom R by A5, FINSEQ_3:27;
hence P . 3 = v2 by A3, A5, A8, GLIB_001:66; :: thesis: ( P . 5 = v3 & P . 7 = v4 )
5 in dom R by A5, FINSEQ_3:27;
hence P . 5 = v3 by A3, A5, A8, GLIB_001:66; :: thesis: P . 7 = v4
P .last() = v4 by A3, A5, A8, GLIB_001:64;
hence P . 7 = v4 by A14; :: thesis: verum