theorem :: GLENUM00:58

for G being _Graph holds
( G is edgeless iff G .allSG() = G .allInducedSG() )