take TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #) ; :: thesis: RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #) #) = RelStr(# the carrier of R, the InternalRel of R #)
thus RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; :: thesis: verum