A1: [#] L is directed by WAYBEL_0:def 6;
RelStr(# the carrier of L,the InternalRel of L #) = RelStr(# the carrier of (L +id ),the InternalRel of (L +id ) #) by Def5;
hence [#] (L +id ) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum