theorem :: GLENUM00:156

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