let G be _Graph; :: thesis: ( G is loopless iff G is GraphUnion of G .allTrees() )

hereby :: thesis: ( G is GraphUnion of G .allTrees() implies G is loopless )

set H = the removeLoops of G;
assume G is loopless ; :: thesis: G is GraphUnion of G .allTrees()
then A1: G == the removeLoops of G by GLIB_009:58;
the removeLoops of G is GraphUnion of G .allTrees() by Th155;
hence G is GraphUnion of G .allTrees() by A1, GLIB_014:22; :: thesis: verum

end;

assume G is GraphUnion of G .allTrees() ; :: thesis: G is loopless
hence G is loopless ; :: thesis: verum