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

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

let z be object ; :: thesis: ( z in G .allTrees() implies z in H .allTrees() )
assume z in G .allTrees() ; :: thesis: z in H .allTrees()
then reconsider H9 = z as Tree-like plain Subgraph of G by Th138;
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 .allTrees() by Th138; :: thesis: verum

end;

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