theorem :: GLIB_000:13

for G being _Graph
for e, x, y being object st e Joins x,y,G holds
( x in the_Vertices_of G & y in the_Vertices_of G ) by FUNCT_2:5;