theorem Th47: :: CHORD:48

for G being _Graph
for v1, v2, v3, v4 being Vertex of G st v1 <> v2 & v1 <> v3 & v2 <> v3 & v2 <> v4 & v3 <> v4 & v1,v2 are_adjacent & v2,v3 are_adjacent & v3,v4 are_adjacent holds
ex P being Path of G st
( len P = 7 & P .length() = 3 & P .vertices() = {v1,v2,v3,v4} & P . 1 = v1 & P . 3 = v2 & P . 5 = v3 & P . 7 = v4 )