let G be loopless connected _Graph; :: thesis: G is GraphUnion of G .allSpanningTrees()
set H = the removeLoops of G;
A1: G == the removeLoops of G by GLIB_009:58;
the removeLoops of G is GraphUnion of G .allSpanningTrees() by Th185;
hence G is GraphUnion of G .allSpanningTrees() by A1, GLIB_014:22; :: thesis: verum