theorem Th14: :: GLENUM00:14

for G being non edgeless _Graph
for e being Edge of G holds e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e