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_reflexive_in the carrier of (L +id) by ORDERS_2:def 2;
hence L +id is reflexive ; :: thesis: verum