let G1, G2 be _Graph; :: thesis: ( G2 in G1 .allInducedSG() iff ex V being non empty Subset of (the_Vertices_of G1) st G2 is plain inducedSubgraph of G1,V )

hereby :: thesis: ( ex V being non empty Subset of (the_Vertices_of G1) st G2 is plain inducedSubgraph of G1,V implies G2 in G1 .allInducedSG() )

assume G2 in G1 .allInducedSG() ; :: thesis: ex V being non empty Subset of (the_Vertices_of G1) st G2 is plain inducedSubgraph of G1,V
then consider V being non empty Subset of (the_Vertices_of G1) such that
A1: G2 = the plain inducedSubgraph of G1,V ;
take V = V; :: thesis: G2 is plain inducedSubgraph of G1,V
thus G2 is plain inducedSubgraph of G1,V by A1; :: thesis: verum

end;

given V being non empty Subset of (the_Vertices_of G1) such that A2: G2 is plain inducedSubgraph of G1,V ; :: thesis: G2 in G1 .allInducedSG()
set H = the plain inducedSubgraph of G1,V;
G2 = the plain inducedSubgraph of G1,V by A2, GLIB_000:93, GLIB_009:44;
hence G2 in G1 .allInducedSG() ; :: thesis: verum