theorem Th111: :: GLENUM00:111

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