theorem :: GLENUM00:122

for G being _Graph holds
( the_Edges_of G = G .loops() iff for H being removeLoops of G holds G .allSpanningForests() = {(H | _GraphSelectors)} )