let G be _Graph; :: thesis: ( the_Edges_of G = G .loops() iff SubtreeRel G = id (G .allTrees()) )
set H = the removeLoops of G;

hereby :: thesis: ( SubtreeRel G = id (G .allTrees()) implies the_Edges_of G = G .loops() )

assume the_Edges_of G = G .loops() ; :: thesis: SubtreeRel G = id (G .allTrees())
then A1: the removeLoops of G is edgeless ;
thus SubtreeRel G = SubtreeRel the removeLoops of G by Th164
.= id ( the removeLoops of G .allTrees()) by A1, Th163
.= id (G .allTrees()) by Th146 ; :: thesis: verum

end;

assume A2: SubtreeRel G = id (G .allTrees()) ; :: thesis: the_Edges_of G = G .loops()
SubtreeRel the removeLoops of G = SubtreeRel G by Th164
.= id ( the removeLoops of G .allTrees()) by A2, Th146 ;
then the removeLoops of G is edgeless by Th163;
hence the_Edges_of G = G .loops() by GLIBPRE1:70; :: thesis: verum