theorem :: GLENUM00:121

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allSpanningForests() is edgeless )