theorem Th38: :: GLENUM00:38

for G being _Graph holds the_Edges_of (G .allSG()) = bool (the_Edges_of G)