A1: RelStr(# the carrier of (x "/\" N),the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N,the InternalRel of N #) by Def3;
A2: [#] N is directed by WAYBEL_0:def 6;
thus [#] (x "/\" N) is directed by A1, A2, WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum