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

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

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

end;

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