theorem Th24: :: GLENUM00:24

for G being edgeless _Graph
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G holds createGraph v in S ) holds
G is Subgraph of G9