A1: SubtreeRel G partially_orders G .allTrees() by Th161;
A2: G .allTrees() = field (SubtreeRel G) by Th160;
thus A3: SubtreeRel G is reflexive by A1, A2, ORDERS_1:def 8, RELAT_2:def 9; :: thesis: ( SubtreeRel G is antisymmetric & SubtreeRel G is transitive & SubtreeRel G is being_partial-order )
thus A4: SubtreeRel G is antisymmetric by A1, A2, ORDERS_1:def 8, RELAT_2:def 12; :: thesis: ( SubtreeRel G is transitive & SubtreeRel G is being_partial-order )
thus SubtreeRel G is transitive by A1, A2, ORDERS_1:def 8, RELAT_2:def 16; :: thesis: SubtreeRel G is being_partial-order
hence SubtreeRel G is being_partial-order by A3, A4, ORDERS_1:def 5; :: thesis: verum