let G be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds H | _GraphSelectors in G .allInducedSG()
let V be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,V holds H | _GraphSelectors in G .allInducedSG()
let H be inducedSubgraph of G,V; :: thesis: H | _GraphSelectors in G .allInducedSG()
H | _GraphSelectors is inducedSubgraph of G,V by GLIB_000:128, GLIB_000:101;
hence H | _GraphSelectors in G .allInducedSG() by Th45; :: thesis: verum