let G be _Graph; :: thesis: ( the_Edges_of G = G .loops() iff G .allSpanningForests() is edgeless )

hereby :: thesis: ( G .allSpanningForests() is edgeless implies the_Edges_of G = G .loops() )

assume the_Edges_of G = G .loops() ; :: thesis: G .allSpanningForests() is edgeless
then A1: G .allForests() is edgeless by Th99;
G .allSpanningForests() = (G .allSpanningSG()) /\ (G .allForests()) by Th103;
hence G .allSpanningForests() is edgeless by A1; :: thesis: verum

end;

assume A2: G .allSpanningForests() is edgeless ; :: thesis: the_Edges_of G = G .loops()

now :: thesis: for x being object st x in the_Edges_of G holds
x in G .loops()

let x be object ; :: thesis: ( x in the_Edges_of G implies x in G .loops() )
assume A3: x in the_Edges_of G ; :: thesis: x in G .loops()
then reconsider G9 = G as non edgeless _Graph ;
reconsider e = x as Edge of G9 by A3;
set H9 = the plain addVertices of createGraph e, the_Vertices_of G;
assume not x in G .loops() ; :: thesis: contradiction
then the plain addVertices of createGraph e, the_Vertices_of G in G .allSpanningForests() by Th107;
hence contradiction by A2; :: thesis: verum

end;

then the_Edges_of G c= G .loops() by TARSKI:def 3;
hence the_Edges_of G = G .loops() by XBOOLE_0:def 10; :: thesis: verum