theorem :: GLENUM00:101

for G being _Graph holds the_Vertices_of (G .allForests()) = (bool (the_Vertices_of G)) \ {{}}