theorem Th109: :: GLENUM00:109

for G1 being _Graph
for G2 being loopless _Graph st G2 .allSpanningForests() c= G1 .allSpanningForests() holds
G2 is spanning Subgraph of G1