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