theorem :: GLENUM00:137

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