theorem :: GLIB_000:66

for G being _Graph
for v1, v2 being Vertex of G
for e being object st e Joins v1,v2,G holds
( v1 .adj e = v2 & v2 .adj e = v1 )