theorem Th99: :: GLENUM00:99

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allForests() is edgeless )