theorem Th80: :: GLENUM00:80

for G being _Graph holds
( G is acyclic iff G | _GraphSelectors in G .allForests() )