theorem Th155: :: GLENUM00:155

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