let G1, G2 be _Graph; :: thesis: for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -isomorphic holds
G1 .allForests() ,G2 .allForests() are_isomorphic
let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2 st G4 is G3 -isomorphic holds
G1 .allForests() ,G2 .allForests() are_isomorphic
let G4 be removeLoops of G2; :: thesis: ( G4 is G3 -isomorphic implies G1 .allForests() ,G2 .allForests() are_isomorphic )
( G1 .allForests() = G3 .allForests() & G2 .allForests() = G4 .allForests() ) by Th87;
hence ( G4 is G3 -isomorphic implies G1 .allForests() ,G2 .allForests() are_isomorphic ) by Th94; :: thesis: verum