theorem Th39: :: ORDERS_5:30

for A being RelStr st the InternalRel of A partially_orders the carrier of A holds
( A is reflexive & A is transitive & A is antisymmetric ) by ORDERS_1:def 8, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;