:: deftheorem defines SubtreeRel GLENUM00:def 13 :
for G being _Graph holds SubtreeRel G = (SubgraphRel G) |_2 (G .allTrees());