let G be _Graph; :: thesis: ( G is acyclic iff G | _GraphSelectors in G .allSpanningForests() )
A1: G .allSpanningForests() = (G .allSpanningSG()) /\ (G .allForests()) by Th103;

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

assume G is acyclic ; :: thesis: G | _GraphSelectors in G .allSpanningForests()
then A2: G | _GraphSelectors in G .allForests() by Th80;
G | _GraphSelectors in G .allSpanningSG() by Th62;
hence G | _GraphSelectors in G .allSpanningForests() by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume G | _GraphSelectors in G .allSpanningForests() ; :: thesis: G is acyclic
then G | _GraphSelectors in G .allForests() by A1;
hence G is acyclic by Th80; :: thesis: verum