theorem Th16: :: GLIB_012:16

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )