theorem Th169: :: GLENUM00:169

for G being _Graph holds G .allSpanningTrees() = (G .allSpanningSG()) /\ (G .allTrees())