let G be _Graph; :: thesis: G | _GraphSelectors in G .allSpanningSG()
reconsider H = G as Subgraph of G by GLIB_000:40;
the_Vertices_of H = the_Vertices_of G ;
then H is spanning by GLIB_000:def 33;
hence G | _GraphSelectors in G .allSpanningSG() by Th61; :: thesis: verum