theorem Th17: :: GLENUM00:17

for G being non edgeless _Graph
for e being Edge of G holds
( createGraph e is loopless iff not e in G .loops() )