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 A6, GLIB_001:91;
then A8: not v3 in (G .walkOf (v1,e1,v2)) .vertices() by A2, A3, TARSKI:def 2;
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 A6, GLIB_001:15;
then A11: ((G .walkOf (v1,e1,v2)) .addEdge e2) .last() = v3 by A9, GLIB_001:63;
A12: (G .walkOf (v1,e1,v2)) .first() = v1 by A6, GLIB_001:15;
then A13: ((G .walkOf (v1,e1,v2)) .addEdge e2) .first() = v1 by A9, A10, GLIB_001:63;
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 A9, A10, A8, GLIB_001:151;
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 A6, GLIB_001:14;
then A15: len P = 3 + 2 by A9, A10, GLIB_001:64;
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:112;
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:108;
then P .edges() = {e1} \/ {e2} by A9, A10, GLIB_001:111;
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 A9, A10, A7, GLIB_001:95;
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 A14, FINSEQ_3:25;
hence P . 3 = (G .walkOf (v1,e1,v2)) . 3 by A9, A10, GLIB_001:65
.= v2 by A6, A10, GLIB_001:14 ;
:: thesis: P . 5 = v3
thus P . 5 = v3 by A11, A15; :: thesis: verum