let R be Relation; :: thesis: ( R is being_partial-order implies R partially_orders field R )
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R and
A3: R is_antisymmetric_in field R ; :: according to RELAT_2:def 9,RELAT_2:def 12,RELAT_2:def 16,ORDERS_1:def 5 :: thesis: R partially_orders field R
thus ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R ) by A1, A2, A3; :: according to ORDERS_1:def 8 :: thesis: verum