let G be _Graph; :: thesis: for v1, v2, v3 being Vertex of G st v1 <> v2 & v1 <> v3 & v2 <> v3 & v1,v2 are_adjacent & v2,v3 are_adjacent holds
ex P being Path of G ex e1, e2 being object st
( P is open & len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )

let v1, v2, v3 be Vertex of G; :: thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 & v1,v2 are_adjacent & v2,v3 are_adjacent implies ex P being Path of G ex e1, e2 being object st
( P is open & len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 ) )

assume that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3 and
A4: v1,v2 are_adjacent and
A5: v2,v3 are_adjacent ; :: thesis: ex P being Path of G ex e1, e2 being object st
( P is open & len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )

consider e1 being object such that
A6: e1 Joins v1,v2,G by A4;
set P1 = G .walkOf (v1,e1,v2);
A7: (G .walkOf (v1,e1,v2)) .vertices() = {v1,v2} by ;
then A8: not v3 in (G .walkOf (v1,e1,v2)) .vertices() by ;
consider e2 being object such that
A9: e2 Joins v2,v3,G by A5;
set P = (G .walkOf (v1,e1,v2)) .addEdge e2;
A10: (G .walkOf (v1,e1,v2)) .last() = v2 by ;
then A11: ((G .walkOf (v1,e1,v2)) .addEdge e2) .last() = v3 by ;
A12: (G .walkOf (v1,e1,v2)) .first() = v1 by ;
then A13: ((G .walkOf (v1,e1,v2)) .addEdge e2) .first() = v1 by ;
G .walkOf (v1,e1,v2) is open by A1, A12, A10;
then reconsider P = (G .walkOf (v1,e1,v2)) .addEdge e2 as Path of G by ;
take P ; :: thesis: ex e1, e2 being object st
( P is open & len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )

take e1 ; :: thesis: ex e2 being object st
( P is open & len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )

take e2 ; :: thesis: ( P is open & len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
thus P is open by A2, A13, A11; :: thesis: ( len P = 5 & P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
A14: len (G .walkOf (v1,e1,v2)) = 3 by ;
then A15: len P = 3 + 2 by ;
hence len P = 5 ; :: thesis: ( P .length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
5 = (2 * ()) + 1 by ;
hence P .length() = 2 ; :: thesis: ( e1 Joins v1,v2,G & e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
thus e1 Joins v1,v2,G by A6; :: thesis: ( e2 Joins v2,v3,G & P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
thus e2 Joins v2,v3,G by A9; :: thesis: ( P .edges() = {e1,e2} & P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
(G .walkOf (v1,e1,v2)) .edges() = {e1} by ;
then P .edges() = {e1} \/ {e2} by ;
hence P .edges() = {e1,e2} by ENUMSET1:1; :: thesis: ( P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
P .vertices() = {v1,v2} \/ {v3} by ;
hence P .vertices() = {v1,v2,v3} by ENUMSET1:3; :: thesis: ( P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
thus P . 1 = v1 by A13; :: thesis: ( P . 3 = v2 & P . 5 = v3 )
3 in dom (G .walkOf (v1,e1,v2)) by ;
hence P . 3 = (G .walkOf (v1,e1,v2)) . 3 by
.= v2 by ;
:: thesis: P . 5 = v3
thus P . 5 = v3 by ; :: thesis: verum