theorem :: SCMYCIEL:42

for G being SimpleGraph holds G = G SubgraphInducedBy (Vertices G)