let G be _Graph; :: thesis: for H being spanning Subgraph of G holds H | _GraphSelectors in G .allSpanningSG()
let H be spanning Subgraph of G; :: thesis: H | _GraphSelectors in G .allSpanningSG()
H | _GraphSelectors == H by GLIB_000:128;
then H | _GraphSelectors is spanning Subgraph of G by GLIB_000:171;
hence H | _GraphSelectors in G .allSpanningSG() by Th60; :: thesis: verum