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