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