theorem Th72: :: GLENUM00:72

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