theorem Th4: :: GLENUM00:4

for G being _Graph
for V being non empty Subset of (the_Vertices_of G) holds createGraph V in G .allSG() by Lm1;