the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;
then A1: the InternalRel of L ~ is_reflexive_in the carrier of L by ORDERS_1:79;
the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6;
hence the InternalRel of (L opp+id) is_reflexive_in the carrier of (L opp+id) by A1, Def6; :: according to ORDERS_2:def 2 :: thesis: verum