let G be _Graph; :: thesis: ( the_Edges_of G = G .loops() iff G .allTrees() = { (createGraph v) where v is Vertex of G : verum } )
set S = { (createGraph v) where v is Vertex of G : verum } ;

hereby :: thesis: ( G .allTrees() = { (createGraph v) where v is Vertex of G : verum } implies the_Edges_of G = G .loops() )

assume the_Edges_of G = G .loops() ; :: thesis: G .allTrees() = { (createGraph v) where v is Vertex of G : verum }
then A1: G .allTrees() is edgeless by Th157;

now :: thesis: for x being object holds
( ( x in G .allTrees() implies x in { (createGraph v) where v is Vertex of G : verum } ) & ( x in { (createGraph v) where v is Vertex of G : verum } implies x in G .allTrees() ) )

let x be object ; :: thesis: ( ( x in G .allTrees() implies x in { (createGraph v) where v is Vertex of G : verum } ) & ( x in { (createGraph v) where v is Vertex of G : verum } implies x in G .allTrees() ) )

hereby :: thesis: ( x in { (createGraph v) where v is Vertex of G : verum } implies x in G .allTrees() )

assume A2: x in G .allTrees() ; :: thesis: x in { (createGraph v) where v is Vertex of G : verum }
then reconsider H = x as Tree-like plain Subgraph of G by Th138;
reconsider V = the_Vertices_of H as non empty Subset of (the_Vertices_of G) ;
set H9 = createGraph V;
reconsider H9 = createGraph V as plain Subgraph of G ;
A3: the_Vertices_of H = the_Vertices_of H9 ;
A4: the_Edges_of H = {} by A1, A2;
then the_Edges_of H = the_Edges_of H9 ;
then ( H is Subgraph of H9 & H9 is Subgraph of H ) by A3, GLIB_000:44;
then A5: H = H9 by GLIB_000:87, GLIB_009:44;
H is edgeless by A4;
then consider v being Vertex of H such that
A6: the_Vertices_of H = {v} by GLIB_000:22;
the_Vertices_of H c= the_Vertices_of G ;
then reconsider v = v as Vertex of G by TARSKI:def 3;
H9 = createGraph v by A6;
hence x in { (createGraph v) where v is Vertex of G : verum } by A5; :: thesis: verum

end;

assume x in { (createGraph v) where v is Vertex of G : verum } ; :: thesis: x in G .allTrees()
then consider v being Vertex of G such that
A7: x = createGraph v ;
thus x in G .allTrees() by A7, Th142; :: thesis: verum

end;

hence G .allTrees() = { (createGraph v) where v is Vertex of G : verum } by TARSKI:2; :: thesis: verum

end;

assume A8: G .allTrees() = { (createGraph v) where v is Vertex of G : verum } ; :: thesis: the_Edges_of G = G .loops()

now :: thesis: for H being _Graph st H in G .allTrees() holds
H is edgeless

let H be _Graph; :: thesis: ( H in G .allTrees() implies H is edgeless )
assume H in G .allTrees() ; :: thesis: H is edgeless
then consider v being Vertex of G such that
A9: H = createGraph v by A8;
thus H is edgeless by A9; :: thesis: verum

end;

then G .allTrees() is edgeless by GLIB_014:def 12;
hence the_Edges_of G = G .loops() by Th157; :: thesis: verum