the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def 3;
then A1: the InternalRel of L ~ is_transitive_in the carrier of L by ORDERS_1:80;
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 ; :: thesis: verum