theorem Th21: :: GLUNIR00:21

for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds VertexDomRel H = (VertexDomRel G) /\ [:V,V:]