let G be _Graph; :: thesis: ( G is connected iff the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)} )

hereby :: thesis: ( the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)} implies G is connected )

assume A1: G is connected ; :: thesis: the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)}
A2: the_Vertices_of (G .allSpanningForests()) = {(the_Vertices_of G)} by Th123;
G .allSpanningTrees() = (G .allConnectedSG()) /\ (G .allSpanningForests()) by Th170;
then G .allSpanningTrees() c= G .allSpanningForests() by XBOOLE_1:17;
then the_Vertices_of (G .allSpanningTrees()) c= {(the_Vertices_of G)} by A2, GLIBPRE1:115;
hence the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)} by A1, ZFMISC_1:33; :: thesis: verum

end;

assume the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)} ; :: thesis: G is connected
hence G is connected ; :: thesis: verum