theorem Th46: :: CHORD:47

for G being _Graph
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 )