let A be RelStr ; :: thesis: ( the InternalRel of A linearly_orders the carrier of A implies ( A is reflexive & A is transitive & A is antisymmetric & A is connected ) )

assume the InternalRel of A linearly_orders the carrier of A ; :: thesis: ( 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_1:def 9;

hence ( A is reflexive & A is transitive & A is antisymmetric & A is connected ) by ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum

assume the InternalRel of A linearly_orders the carrier of A ; :: thesis: ( 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_1:def 9;

hence ( A is reflexive & A is transitive & A is antisymmetric & A is connected ) by ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum