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

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

set H = the removeLoops of G;
assume A1: the_Edges_of G = G .loops() ; :: thesis: G .allTrees() is edgeless

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 A2: H is Tree-like Subgraph of G by Th138;

now :: thesis: not the_Edges_of H <> {}

assume the_Edges_of H <> {} ; :: thesis: contradiction
then consider e being object such that
A3: e in the_Edges_of H by XBOOLE_0:def 1;
the_Edges_of H c= the_Edges_of G by A2, GLIB_000:def 32;
then consider v being object such that
A4: e Joins v,v,G by A1, A3, GLIB_009:def 2;
( e is set & v is set ) by TARSKI:1;
then e Joins v,v,H by A2, A3, A4, GLIB_000:73;
hence contradiction by A2, GLIB_000:18; :: thesis: verum

end;

hence H is edgeless ; :: thesis: verum

end;

hence G .allTrees() is edgeless by GLIB_014:def 12; :: thesis: verum

end;

assume A5: G .allTrees() 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 A6: 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 A6;
set H9 = createGraph e;
assume not x in G .loops() ; :: thesis: contradiction
then createGraph e in G .allTrees() by Th143;
hence contradiction by A5; :: 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