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