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

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

assume A1: G3 == G4 ; :: thesis: G1 .allTrees() = G2 .allTrees()
thus G1 .allTrees() = G3 .allTrees() by Th146
.= G4 .allTrees() by A1, Th147
.= G2 .allTrees() by Th146 ; :: thesis: verum

end;

assume A2: G1 .allTrees() = G2 .allTrees() ; :: thesis: G3 == G4
G3 .allTrees() = G1 .allTrees() by Th146
.= G4 .allTrees() by A2, Th146 ;
hence G3 == G4 by Th147; :: thesis: verum