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 set st
( not P is closed & 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 set st
( not P is closed & 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 & v1 <> v3 ) and
A2: v2 <> v3 and
A3: v1,v2 are_adjacent and
A4: v2,v3 are_adjacent ; :: thesis: ex P being Path of G ex e1, e2 being set st
( not P is closed & 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 set such that
A5: e1 Joins v1,v2,G by A3, Def3;
consider e2 being set such that
A6: e2 Joins v2,v3,G by A4, Def3;
set P1 = G .walkOf v1,e1,v2;
A7: (G .walkOf v1,e1,v2) .first() = v1 by A5, GLIB_001:16;
A8: (G .walkOf v1,e1,v2) .last() = v2 by A5, GLIB_001:16;
A9: len (G .walkOf v1,e1,v2) = 3 by A5, GLIB_001:15;
A10: (G .walkOf v1,e1,v2) .vertices() = {v1,v2} by A5, GLIB_001:92;
A11: not G .walkOf v1,e1,v2 is closed by A1, A7, A8, GLIB_001:def 24;
set P = (G .walkOf v1,e1,v2) .addEdge e2;
A12: ((G .walkOf v1,e1,v2) .addEdge e2) .first() = v1 by A6, A7, A8, GLIB_001:64;
A13: ((G .walkOf v1,e1,v2) .addEdge e2) .last() = v3 by A6, A8, GLIB_001:64;
not v3 in (G .walkOf v1,e1,v2) .vertices() by A1, A2, A10, TARSKI:def 2;
then reconsider P = (G .walkOf v1,e1,v2) .addEdge e2 as Path of G by A6, A8, A11, GLIB_001:152;
take P ; :: thesis: ex e1, e2 being set st
( not P is closed & 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 set st
( not P is closed & 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: ( not P is closed & 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 not P is closed by A1, A12, A13, GLIB_001:def 24; :: 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 P = 3 + 2 by A6, A8, A9, GLIB_001:65;
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 * (P .length() )) + 1 by A14, GLIB_001:113;
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 A5; :: 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 A6; :: 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 A5, GLIB_001:109;
then P .edges() = {e1} \/ {e2} by A6, A8, GLIB_001:112;
hence P .edges() = {e1,e2} by ENUMSET1:41; :: thesis: ( P .vertices() = {v1,v2,v3} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
P .vertices() = {v1,v2} \/ {v3} by A6, A8, A10, GLIB_001:96;
hence P .vertices() = {v1,v2,v3} by ENUMSET1:43; :: thesis: ( P . 1 = v1 & P . 3 = v2 & P . 5 = v3 )
thus P . 1 = v1 by A12; :: thesis: ( P . 3 = v2 & P . 5 = v3 )
3 in dom (G .walkOf v1,e1,v2) by A9, FINSEQ_3:27;
hence P . 3 = (G .walkOf v1,e1,v2) . 3 by A6, A8, GLIB_001:66
.= v2 by A5, A8, GLIB_001:15 ;
:: thesis: P . 5 = v3
thus P . 5 = v3 by A13, A14; :: thesis: verum