theorem Th57: :: GLENUM00:57

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