let G1, G2 be _Graph; :: thesis: for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allSpanningForests() = G2 .allSpanningForests() )
let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allSpanningForests() = G2 .allSpanningForests() )
let G4 be removeLoops of G2; :: thesis: ( G3 == G4 iff G1 .allSpanningForests() = G2 .allSpanningForests() )

hereby :: thesis: ( G1 .allSpanningForests() = G2 .allSpanningForests() implies G3 == G4 )

assume A1: G3 == G4 ; :: thesis: G1 .allSpanningForests() = G2 .allSpanningForests()
thus G1 .allSpanningForests() = G3 .allSpanningForests() by Th110
.= G4 .allSpanningForests() by A1, Th111
.= G2 .allSpanningForests() by Th110 ; :: thesis: verum

end;

assume A2: G1 .allSpanningForests() = G2 .allSpanningForests() ; :: thesis: G3 == G4
G3 .allSpanningForests() = G1 .allSpanningForests() by Th110
.= G4 .allSpanningForests() by A2, Th110 ;
hence G3 == G4 by Th111; :: thesis: verum