theorem :: GLENUM00:112

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allSpanningForests() = G2 .allSpanningForests() )