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