let G be _Graph; :: thesis: for H being removeLoops of G holds H is GraphUnion of G .allSpanningForests()
let H be removeLoops of G; :: thesis: H is GraphUnion of G .allSpanningForests()
set G9 = the GraphUnion of G .allSpanningForests() ;
reconsider G8 = G as GraphUnion of G .allSG() by Th35;
set H9 = the GraphUnion of {H};

now :: thesis: ( the GraphUnion of G .allSpanningForests() is Subgraph of G8 & the_Vertices_of H c= the_Vertices_of the GraphUnion of G .allSpanningForests() & the_Edges_of H c= the_Edges_of the GraphUnion of G .allSpanningForests() )

thus the GraphUnion of G .allSpanningForests() is Subgraph of G8 by GLIBPRE1:119; :: thesis: ( the_Vertices_of H c= the_Vertices_of the GraphUnion of G .allSpanningForests() & the_Edges_of H c= the_Edges_of the GraphUnion of G .allSpanningForests() )

now :: thesis: for x being object st x in the_Vertices_of H holds
x in the_Vertices_of the GraphUnion of G .allSpanningForests()

let x be object ; :: thesis: ( x in the_Vertices_of H implies x in the_Vertices_of the GraphUnion of G .allSpanningForests() )
assume x in the_Vertices_of H ; :: thesis: x in the_Vertices_of the GraphUnion of G .allSpanningForests()
then A1: x in the_Vertices_of G ;
set H8 = createGraph ([#] (the_Vertices_of G));
createGraph ([#] (the_Vertices_of G)) in G .allSpanningForests() by Th106;
then createGraph ([#] (the_Vertices_of G)) is Subgraph of the GraphUnion of G .allSpanningForests() by GLIB_014:21;
then the_Vertices_of (createGraph ([#] (the_Vertices_of G))) c= the_Vertices_of the GraphUnion of G .allSpanningForests() by GLIB_000:def 32;
hence x in the_Vertices_of the GraphUnion of G .allSpanningForests() by A1; :: thesis: verum

end;

hence the_Vertices_of H c= the_Vertices_of the GraphUnion of G .allSpanningForests() by TARSKI:def 3; :: thesis: the_Edges_of H c= the_Edges_of the GraphUnion of G .allSpanningForests()

now :: thesis: for x being object st x in the_Edges_of H holds
x in the_Edges_of the GraphUnion of G .allSpanningForests()

let x be object ; :: thesis: ( x in the_Edges_of H implies x in the_Edges_of the GraphUnion of G .allSpanningForests() )
assume x in the_Edges_of H ; :: thesis: x in the_Edges_of the GraphUnion of G .allSpanningForests()
then x in (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
then A2: ( x in the_Edges_of G & not x in G .loops() ) by XBOOLE_0:def 5;
then reconsider G0 = G as non edgeless _Graph ;
reconsider e = x as Edge of G0 by A2;
set H8 = the plain addVertices of createGraph e, the_Vertices_of G;
the plain addVertices of createGraph e, the_Vertices_of G in G .allSpanningForests() by A2, Th107;
then the plain addVertices of createGraph e, the_Vertices_of G is Subgraph of the GraphUnion of G .allSpanningForests() by GLIB_014:21;
then the_Edges_of the plain addVertices of createGraph e, the_Vertices_of G c= the_Edges_of the GraphUnion of G .allSpanningForests() by GLIB_000:def 32;
then the_Edges_of (createGraph e) c= the_Edges_of the GraphUnion of G .allSpanningForests() by GLIB_006:def 10;
then {e} c= the_Edges_of the GraphUnion of G .allSpanningForests() by Th13;
hence x in the_Edges_of the GraphUnion of G .allSpanningForests() by ZFMISC_1:31; :: thesis: verum

end;

hence the_Edges_of H c= the_Edges_of the GraphUnion of G .allSpanningForests() by TARSKI:def 3; :: thesis: verum

end;

then A3: H is Subgraph of the GraphUnion of G .allSpanningForests() by GLIB_000:44;

now :: thesis: for H2 being Element of G .allSpanningForests() ex H1 being Element of {H} st H2 is Subgraph of H1

let H2 be Element of G .allSpanningForests() ; :: thesis: ex H1 being Element of {H} st H2 is Subgraph of H1
reconsider H1 = H as Element of {H} by TARSKI:def 1;
take H1 = H1; :: thesis: H2 is Subgraph of H1
H .allSpanningForests() = G .allSpanningForests() by Th110;
hence H2 is Subgraph of H1 by Th102; :: thesis: verum

end;

then the GraphUnion of G .allSpanningForests() is Subgraph of the GraphUnion of {H} by GLIBPRE1:118;
then the GraphUnion of G .allSpanningForests() is Subgraph of H by GLIB_000:91, GLIB_014:24;
hence H is GraphUnion of G .allSpanningForests() by A3, GLIB_000:87, GLIB_014:22; :: thesis: verum