:: deftheorem defines SubgraphInducedBy SCMYCIEL:def 12 :
for G being SimpleGraph
for L being set holds G SubgraphInducedBy L = G /\ (bool L);