let G be _Graph; :: thesis: for H being spanning acyclic Subgraph of G holds H | _GraphSelectors in G .allSpanningForests()
let H be spanning acyclic Subgraph of G; :: thesis: H | _GraphSelectors in G .allSpanningForests()
H | _GraphSelectors == H by GLIB_000:128;
then H | _GraphSelectors is spanning acyclic Subgraph of G by GLIB_000:171, GLIB_002:44;
hence H | _GraphSelectors in G .allSpanningForests() by Th102; :: thesis: verum