theorem :: GLIB_000:65

for G being _Graph
for v being Vertex of G
for e, x, y being object st e in v .edgesInOut() & e Joins x,y,G & not v = x holds
v = y