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

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

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

A22:
e2 <> e3
by A4, A18, A12;
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

end;assume that

A20: 1 < n and

A21: n <= len R ; :: thesis: R . n <> v4

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