let A be LinearOrder; :: thesis: the InternalRel of A linearly_orders the carrier of A

( A is reflexive & A is transitive & A is antisymmetric & A is connected ) ;

then ( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A & the InternalRel of A is_connected_in the carrier of A ) by ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

hence the InternalRel of A linearly_orders the carrier of A by ORDERS_1:def 9; :: thesis: verum

( A is reflexive & A is transitive & A is antisymmetric & A is connected ) ;

then ( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A & the InternalRel of A is_connected_in the carrier of A ) by ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

hence the InternalRel of A linearly_orders the carrier of A by ORDERS_1:def 9; :: thesis: verum