theorem :: GLIB_000:120

for G1 being _Graph
for V being set
for G2 being inducedSubgraph of G1,V st G2 is spanning holds
G1 == G2