let G be _Graph; :: thesis: for H being removeLoops of G holds G .allSpanningTrees() = H .allSpanningTrees()
let H be removeLoops of G; :: thesis: G .allSpanningTrees() = H .allSpanningTrees()

per cases ( G is connected or not G is connected ) ;

suppose A1: G is connected ; :: thesis: G .allSpanningTrees() = H .allSpanningTrees()

A2: H .allSpanningTrees() c= G .allSpanningTrees() by A1, Th174;

now :: thesis: for x being object st x in G .allSpanningTrees() holds
x in H .allSpanningTrees()

let x be object ; :: thesis: ( x in G .allSpanningTrees() implies x in H .allSpanningTrees() )
assume A3: x in G .allSpanningTrees() ; :: thesis: x in H .allSpanningTrees()
then reconsider G2 = x as spanning acyclic plain Subgraph of G by Th168;
A4: G2 is connected by A3, Th168;
A5: the_Vertices_of G2 = the_Vertices_of G by GLIB_000:def 33
.= the_Vertices_of H by GLIB_000:def 33 ;
A6: the_Edges_of H = (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
(the_Edges_of G2) /\ (G .loops()) = {}

proof

assume (the_Edges_of G2) /\ (G .loops()) <> {} ; :: thesis: contradiction
then consider y being object such that
A7: y in (the_Edges_of G2) /\ (G .loops()) by XBOOLE_0:def 1;
A8: ( y in the_Edges_of G2 & y in G .loops() ) by A7, XBOOLE_0:def 4;
then consider v being object such that
A9: y Joins v,v,G by GLIB_009:def 2;
( y is set & v is set ) by TARSKI:1;
then y Joins v,v,G2 by A8, A9, GLIB_000:73;
then y in G2 .loops() by GLIB_009:def 2;
hence contradiction ; :: thesis: verum

end;

then the_Edges_of G2 c= the_Edges_of H by A6, XBOOLE_0:def 7, XBOOLE_1:86;
then reconsider G2 = G2 as spanning Subgraph of H by A5, GLIB_000:def 33, GLIB_000:44;
G2 is Tree-like by A4;
hence x in H .allSpanningTrees() by Th168; :: thesis: verum

end;

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

end;

suppose not G is connected ; :: thesis: G .allSpanningTrees() = H .allSpanningTrees()

then ( G .allSpanningTrees() = {} & H .allSpanningTrees() = {} ) ;
hence G .allSpanningTrees() = H .allSpanningTrees() ; :: thesis: verum

end;

end;