theorem :: GLENUM00:98

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