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

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

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

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

let x be object ; :: thesis: ( x in the_Vertices_of H implies x in the_Vertices_of the GraphUnion of G .allSpanningTrees() )
set H8 = the Element of G .allSpanningTrees() ;
assume x in the_Vertices_of H ; :: thesis: x in the_Vertices_of the GraphUnion of G .allSpanningTrees()
then A1: x in the_Vertices_of G ;
the Element of G .allSpanningTrees() is spanning by Th168;
then A2: x in the_Vertices_of the Element of G .allSpanningTrees() by A1, GLIB_000:def 33;
the Element of G .allSpanningTrees() is Subgraph of the GraphUnion of G .allSpanningTrees() by GLIB_014:21;
then the_Vertices_of the Element of G .allSpanningTrees() c= the_Vertices_of the GraphUnion of G .allSpanningTrees() by GLIB_000:def 32;
hence x in the_Vertices_of the GraphUnion of G .allSpanningTrees() by A2; :: thesis: verum

end;

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

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

let x be object ; :: thesis: ( x in the_Edges_of H implies x in the_Edges_of the GraphUnion of G .allSpanningTrees() )
assume x in the_Edges_of H ; :: thesis: x in the_Edges_of the GraphUnion of G .allSpanningTrees()
then x in (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
then consider T being spanning Tree-like plain Subgraph of G such that
A3: x in the_Edges_of T by Th167;
T in G .allSpanningTrees() by Th168;
then T is Subgraph of the GraphUnion of G .allSpanningTrees() by GLIB_014:21;
then the_Edges_of T c= the_Edges_of the GraphUnion of G .allSpanningTrees() by GLIB_000:def 32;
hence x in the_Edges_of the GraphUnion of G .allSpanningTrees() by A3; :: thesis: verum

end;

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

end;

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

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

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

end;

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