theorem Th75: :: GLIB_006:71

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