theorem :: GLIB_012:22

for G being _Graph holds G is addLoops of G, {}