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