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

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

assume A1: G3 == G4 ; :: thesis: G1 .allForests() = G2 .allForests()
thus G1 .allForests() = G3 .allForests() by Th87
.= G4 .allForests() by A1, Th88
.= G2 .allForests() by Th87 ; :: thesis: verum

end;

assume A2: G1 .allForests() = G2 .allForests() ; :: thesis: G3 == G4
G3 .allForests() = G1 .allForests() by Th87
.= G4 .allForests() by A2, Th87 ;
hence G3 == G4 by Th88; :: thesis: verum