theorem Th101: :: GLIB_000:101

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