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

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

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

end;

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