theorem Th88: :: GLENUM00:88

for G1, G2 being loopless _Graph holds
( G1 == G2 iff G1 .allForests() = G2 .allForests() )