theorem Th147: :: GLENUM00:147

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