let G be _Graph; :: thesis: ( G is acyclic iff G | _GraphSelectors in G .allForests() )

hereby :: thesis: ( G | _GraphSelectors in G .allForests() implies G is acyclic )

assume A1: G is acyclic ; :: thesis: G | _GraphSelectors in G .allForests()
G is Subgraph of G by GLIB_000:40;
hence G | _GraphSelectors in G .allForests() by A1, Th79; :: thesis: verum

end;

assume G | _GraphSelectors in G .allForests() ; :: thesis: G is acyclic
then A2: G | _GraphSelectors is acyclic by Th78;
G | _GraphSelectors == G by GLIB_000:128;
hence G is acyclic by A2, GLIB_002:44; :: thesis: verum