theorem :: GLIBPRE1:70

for G being _Graph
for H being removeLoops of G holds
( the_Edges_of G = G .loops() iff H is edgeless )