let G be _Graph; :: thesis: for H being acyclic Subgraph of G holds H | _GraphSelectors in G .allForests()
let H be acyclic Subgraph of G; :: thesis: H | _GraphSelectors in G .allForests()
H | _GraphSelectors is acyclic Subgraph of G by GLIB_000:92, GLIB_002:44, GLIB_000:128;
hence H | _GraphSelectors in G .allForests() by Th78; :: thesis: verum