let G be _Graph; :: thesis: ( the_Edges_of G = G .loops() iff G .allForests() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } )
set S = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ;

hereby :: thesis: ( G .allForests() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies the_Edges_of G = G .loops() )

assume the_Edges_of G = G .loops() ; :: thesis: G .allForests() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum }
then A1: G .allForests() is edgeless by Th99;

now :: thesis: for x being object holds
( ( x in G .allForests() implies x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ) & ( x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allForests() ) )

let x be object ; :: thesis: ( ( x in G .allForests() implies x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ) & ( x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allForests() ) )

hereby :: thesis: ( x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allForests() )

assume A2: x in G .allForests() ; :: thesis: x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum }
then reconsider H = x as plain Subgraph of G by Th78;
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 ;
the_Edges_of H = the_Edges_of H9 by A1, A2;
then ( H is Subgraph of H9 & H9 is Subgraph of H ) by A3, GLIB_000:44;
then H = H9 by GLIB_000:87, GLIB_009:44;
hence x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: verum

end;

assume x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: x in G .allForests()
then consider V being non empty Subset of (the_Vertices_of G) such that
A4: x = createGraph V ;
thus x in G .allForests() by A4, Th81; :: thesis: verum

end;

hence G .allForests() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } by TARSKI:2; :: thesis: verum

end;

assume A5: G .allForests() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: the_Edges_of G = G .loops()

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

let H be _Graph; :: thesis: ( H in G .allForests() implies H is edgeless )
assume H in G .allForests() ; :: thesis: H is edgeless
then consider V being non empty Subset of (the_Vertices_of G) such that
A6: H = createGraph V by A5;
thus H is edgeless by A6; :: thesis: verum

end;

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