theorem :: GLENUM00:59

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