let G be _Graph; :: thesis: G | _GraphSelectors in G .allSG()
G is Subgraph of G by GLIB_000:40;
hence G | _GraphSelectors in G .allSG() by Th2; :: thesis: verum