theorem Th45: :: SCMYCIEL:45

for G being SimpleGraph
for L being set holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L