let G2 be _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 )
let G1 be 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 )
let e, v1, v2 be object ; ( not e DJoins v1,v2,G1 or e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
assume A1:
e DJoins v1,v2,G1
; ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 )