theorem Th45: :: GLENUM00:45

for G1, G2 being _Graph holds
( G2 in G1 .allInducedSG() iff ex V being non empty Subset of (the_Vertices_of G1) st G2 is plain inducedSubgraph of G1,V )