take RelStr(# [:the carrier of X,the carrier of Y:],["the InternalRel of X,the InternalRel of Y"] #) ; :: thesis: ( the carrier of RelStr(# [:the carrier of X,the carrier of Y:],["the InternalRel of X,the InternalRel of Y"] #) = [:the carrier of X,the carrier of Y:] & the InternalRel of RelStr(# [:the carrier of X,the carrier of Y:],["the InternalRel of X,the InternalRel of Y"] #) = ["the InternalRel of X,the InternalRel of Y"] )
thus ( the carrier of RelStr(# [:the carrier of X,the carrier of Y:],["the InternalRel of X,the InternalRel of Y"] #) = [:the carrier of X,the carrier of Y:] & the InternalRel of RelStr(# [:the carrier of X,the carrier of Y:],["the InternalRel of X,the InternalRel of Y"] #) = ["the InternalRel of X,the InternalRel of Y"] ) ; :: thesis: verum