let G be _Graph; :: thesis: for H being removeLoops of G holds G .allForests() = H .allForests()
let H be removeLoops of G; :: thesis: G .allForests() = H .allForests()
A1: H .allForests() c= G .allForests() by Th85;

now :: thesis: for z being object st z in G .allForests() holds
z in H .allForests()

let z be object ; :: thesis: ( z in G .allForests() implies z in H .allForests() )
assume z in G .allForests() ; :: thesis: z in H .allForests()
then reconsider H9 = z as acyclic plain Subgraph of G by Th78;
the_Vertices_of H9 c= the_Vertices_of G ;
then A2: the_Vertices_of H9 c= the_Vertices_of H by GLIB_000:def 33;

now :: thesis: for x being object st x in the_Edges_of H9 holds
x in the_Edges_of H

let x be object ; :: thesis: ( x in the_Edges_of H9 implies x in the_Edges_of H )
assume A3: x in the_Edges_of H9 ; :: thesis: x in the_Edges_of H
then A4: x in the_Edges_of G ;
not x in G .loops()

proof

assume x in G .loops() ; :: thesis: contradiction
then consider v being object such that
A5: x Joins v,v,G by GLIB_009:def 2;
( x is set & v is set ) by TARSKI:1;
then x Joins v,v,H9 by A3, A5, GLIB_000:73;
then x in H9 .loops() by GLIB_009:def 2;
hence contradiction ; :: thesis: verum

end;

then x in (the_Edges_of G) \ (G .loops()) by A4, XBOOLE_0:def 5;
hence x in the_Edges_of H by GLIB_000:53; :: thesis: verum

end;

then the_Edges_of H9 c= the_Edges_of H by TARSKI:def 3;
then H9 is Subgraph of H by A2, GLIB_000:44;
hence z in H .allForests() by Th78; :: thesis: verum

end;

then G .allForests() c= H .allForests() by TARSKI:def 3;
hence G .allForests() = H .allForests() by A1, XBOOLE_0:def 10; :: thesis: verum