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

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

assume A1: G2 .allInducedSG() c= G1 .allInducedSG() ; :: thesis: ex V being non empty Subset of (the_Vertices_of G1) st G2 is inducedSubgraph of G1,V
G2 | _GraphSelectors in G2 .allInducedSG() by Th47;
then consider V being non empty Subset of (the_Vertices_of G1) such that
A2: G2 | _GraphSelectors is plain inducedSubgraph of G1,V by A1, Th45;
take V = V; :: thesis: G2 is inducedSubgraph of G1,V
G2 == G2 | _GraphSelectors by GLIB_000:128;
hence G2 is inducedSubgraph of G1,V by A2, GLIB_000:101; :: thesis: verum

end;

given V being non empty Subset of (the_Vertices_of G1) such that A3: G2 is inducedSubgraph of G1,V ; :: thesis: G2 .allInducedSG() c= G1 .allInducedSG()

now :: thesis: for x being object st x in G2 .allInducedSG() holds
x in G1 .allInducedSG()

let x be object ; :: thesis: ( x in G2 .allInducedSG() implies x in G1 .allInducedSG() )
assume x in G2 .allInducedSG() ; :: thesis: x in G1 .allInducedSG()
then consider V2 being non empty Subset of (the_Vertices_of G2) such that
A4: x is plain inducedSubgraph of G2,V2 by Th45;
the_Vertices_of G2 = V by A3, GLIB_000:def 37;
then A5: V2 c= V ;
then A6: V2 is non empty Subset of (the_Vertices_of G1) by XBOOLE_1:1;
then x is inducedSubgraph of G1,V2 by A3, A4, A5, CHORD:29;
hence x in G1 .allInducedSG() by A4, A6, Th45; :: thesis: verum

end;

hence G2 .allInducedSG() c= G1 .allInducedSG() by TARSKI:def 3; :: thesis: verum