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