theorem :: GLENUM00:188

for G being _Graph holds
( G is connected iff the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)} )