theorem Th9: :: GLENUM00:9

for G being _Graph holds
( G is edgeless iff G .allSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } )