let G be _Graph; :: thesis: SubtreeRel G partially_orders G .allTrees()
SubgraphRel G partially_orders G .allTrees() by Th41, ORDERS_1:35;
then SubtreeRel G is being_partial-order by ORDERS_1:36;
then SubtreeRel G partially_orders field (SubtreeRel G) by ORDERS_1:34;
hence SubtreeRel G partially_orders G .allTrees() by Th160; :: thesis: verum