theorem Th119: :: GLENUM00:119

for G being _Graph
for H being removeLoops of G holds H is GraphUnion of G .allSpanningForests()