theorem Th97: :: GLENUM00:97

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