( RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) & [#] N is directed )
by Def3, WAYBEL_0:def 6;

hence [#] (x "/\" N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum

hence [#] (x "/\" N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum