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