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

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

let z be object ; :: thesis: ( z in G .allSpanningForests() implies z in H .allSpanningForests() )
assume z in G .allSpanningForests() ; :: thesis: z in H .allSpanningForests()
then reconsider H9 = z as spanning acyclic plain Subgraph of G by Th102;
A2: the_Vertices_of H9 = the_Vertices_of G by GLIB_000:def 33
.= 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 spanning Subgraph of H by A2, GLIB_000:44, GLIB_000:def 33;
hence z in H .allSpanningForests() by Th102; :: thesis: verum

end;

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