theorem Th163: :: GLENUM00:163

for G being loopless _Graph holds
( G is edgeless iff SubtreeRel G = id (G .allTrees()) )