let G be _Graph; :: thesis: G | _GraphSelectors in G .allInducedSG()
the_Vertices_of G c= the_Vertices_of G ;
then A1: the_Vertices_of G is non empty Subset of (the_Vertices_of G) ;
G is inducedSubgraph of G,(the_Vertices_of G) by GLIB_000:100;
hence G | _GraphSelectors in G .allInducedSG() by A1, Th46; :: thesis: verum