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 .allTrees() ,G2 .allTrees() are_Disomorphic
let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2 st G4 is G3 -Disomorphic holds
G1 .allTrees() ,G2 .allTrees() are_Disomorphic
let G4 be removeLoops of G2; :: thesis: ( G4 is G3 -Disomorphic implies G1 .allTrees() ,G2 .allTrees() are_Disomorphic )
( G1 .allTrees() = G3 .allTrees() & G2 .allTrees() = G4 .allTrees() ) by Th146;
hence ( G4 is G3 -Disomorphic implies G1 .allTrees() ,G2 .allTrees() are_Disomorphic ) by Th151; :: thesis: verum