theorem :: GLENUM00:148
for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allTrees() = G2 .allTrees() )