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

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

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

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

let x be object ; :: thesis: ( x in the_Vertices_of H implies x in the_Vertices_of the GraphUnion of G .allForests() )
assume x in the_Vertices_of H ; :: thesis: x in the_Vertices_of the GraphUnion of G .allForests()
then reconsider v = x as Vertex of G ;
set H8 = createGraph v;
createGraph v in G .allForests() by Th82;
then createGraph v is Subgraph of the GraphUnion of G .allForests() by GLIB_014:21;
then the_Vertices_of (createGraph v) c= the_Vertices_of the GraphUnion of G .allForests() by GLIB_000:def 32;
hence x in the_Vertices_of the GraphUnion of G .allForests() by ZFMISC_1:31; :: thesis: verum

end;

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

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

let x be object ; :: thesis: ( x in the_Edges_of H implies x in the_Edges_of the GraphUnion of G .allForests() )
assume x in the_Edges_of H ; :: thesis: x in the_Edges_of the GraphUnion of G .allForests()
then x in (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
then A1: ( 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 A1;
set H8 = createGraph e;
createGraph e in G .allForests() by A1, Th83;
then createGraph e is Subgraph of the GraphUnion of G .allForests() by GLIB_014:21;
then the_Edges_of (createGraph e) c= the_Edges_of the GraphUnion of G .allForests() by GLIB_000:def 32;
then {e} c= the_Edges_of the GraphUnion of G .allForests() by Th13;
hence x in the_Edges_of the GraphUnion of G .allForests() by ZFMISC_1:31; :: thesis: verum

end;

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

end;

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

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

let H2 be Element of G .allForests() ; :: 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 .allForests() = G .allForests() by Th87;
hence H2 is Subgraph of H1 by Th78; :: thesis: verum

end;

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