let G1, G2 be _Graph; :: thesis: ( G2 in G1 .allSpanningForests() iff G2 is spanning acyclic plain Subgraph of G1 )

hereby :: thesis: ( G2 is spanning acyclic plain Subgraph of G1 implies G2 in G1 .allSpanningForests() )

assume G2 in G1 .allSpanningForests() ; :: thesis: G2 is spanning acyclic plain Subgraph of G1
then consider H being Element of [#] (G1 .allSG()) such that
A1: ( G2 = H & H is spanning & H is acyclic ) ;
thus G2 is spanning acyclic plain Subgraph of G1 by A1; :: thesis: verum

end;

assume A2: G2 is spanning acyclic plain Subgraph of G1 ; :: thesis: G2 in G1 .allSpanningForests()
then G2 in [#] (G1 .allSG()) by Th1;
hence G2 in G1 .allSpanningForests() by A2; :: thesis: verum