let G be _Graph; :: thesis: for H being Subgraph of G holds H | _GraphSelectors in G .allSG()
let H be Subgraph of G; :: thesis: H | _GraphSelectors in G .allSG()
H | _GraphSelectors is Subgraph of G by GLIB_000:92, GLIB_000:128;
hence H | _GraphSelectors in G .allSG() by Th1; :: thesis: verum