theorem Th62: :: GLIB_000:62

for G being _Graph
for v1 being Vertex of G
for e, x being object st e Joins v1,x,G holds
e in v1 .edgesInOut() by Th61;