RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;
hence not x "/\" N is empty ; :: thesis: verum