theorem Th138: :: GLENUM00:138

for G1, G2 being _Graph holds
( G2 in G1 .allTrees() iff G2 is Tree-like plain Subgraph of G1 )