theorem Th37: :: GLENUM00:37

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