theorem Th177: :: GLENUM00:177

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