theorem Th55: :: GLENUM00:55

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