theorem Th175: :: GLENUM00:175
for G1 being _Graph
for G2 being loopless connected _Graph st G2 .allSpanningTrees() c= G1 .allSpanningTrees() holds
G2 is spanning Subgraph of G1