the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def 5;
then A1: the InternalRel of L ~ is_transitive_in the carrier of L by ORDERS_1:190;
the InternalRel of (L opp+id ) = the InternalRel of L ~ by Def6;
then the InternalRel of (L opp+id ) is_transitive_in the carrier of (L opp+id ) by A1, Def6;
hence L opp+id is transitive by ORDERS_2:def 5; :: thesis: verum