the InternalRel of L is_antisymmetric_in the carrier of L by ORDERS_2:def 6;
then A1: the InternalRel of L ~ is_antisymmetric_in the carrier of L by ORDERS_1:191;
the InternalRel of (L opp+id ) = the InternalRel of L ~ by Def6;
then the InternalRel of (L opp+id ) is_antisymmetric_in the carrier of (L opp+id ) by A1, Def6;
hence L opp+id is antisymmetric by ORDERS_2:def 6; :: thesis: verum