theorem :: GLENUM00:120

for G being _Graph holds
( G is loopless iff G is GraphUnion of G .allSpanningForests() )