RelStr(# the carrier of L,the InternalRel of L #) = RelStr(# the carrier of (L +id ),the InternalRel of (L +id ) #) by Def5;
then the InternalRel of (L +id ) is_antisymmetric_in the carrier of (L +id ) by ORDERS_2:def 6;
hence L +id is antisymmetric by ORDERS_2:def 6; :: thesis: verum