theorem Th7: :: GLENUM00:7

for G being _Graph holds
( G is edgeless iff G == createGraph ([#] (the_Vertices_of G)) )