theorem Th35: :: GLENUM00:35

for G being _Graph holds G is GraphUnion of G .allSG()