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