theorem Th76: :: GLIB_006:72

for G2 being _Graph
for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e Joins v1,v2,G1 or e Joins v1,v2,G2 or not e in the_Edges_of G2 )