theorem Th123: :: GLENUM00:123

for G being _Graph holds the_Vertices_of (G .allSpanningForests()) = {(the_Vertices_of G)}