let G1, G2 be _Graph; :: thesis: ( G2 in G1 .allTrees() iff G2 is Tree-like plain Subgraph of G1 )

hereby :: thesis: ( G2 is Tree-like plain Subgraph of G1 implies G2 in G1 .allTrees() )

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

end;

assume A2: G2 is Tree-like plain Subgraph of G1 ; :: thesis: G2 in G1 .allTrees()
then G2 in [#] (G1 .allSG()) by Th1;
hence G2 in G1 .allTrees() by A2; :: thesis: verum