for G1 being _Graph
for G3 being Subgraph of G1
for v, e, w being object
for G2 being addEdge of G3,v,e,w st e DJoins v,w,G1 holds
G2 is Subgraph of G1