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