theorem :: GLENUM00:89

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