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