take RelStr(# the carrier of R,(the InternalRel of R \/ (the InternalRel of R ~ )) #) ; :: thesis: ( the carrier of RelStr(# the carrier of R,(the InternalRel of R \/ (the InternalRel of R ~ )) #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,(the InternalRel of R \/ (the InternalRel of R ~ )) #) = the InternalRel of R \/ (the InternalRel of R ~ ) )
thus ( the carrier of RelStr(# the carrier of R,(the InternalRel of R \/ (the InternalRel of R ~ )) #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,(the InternalRel of R \/ (the InternalRel of R ~ )) #) = the InternalRel of R \/ (the InternalRel of R ~ ) ) ; :: thesis: verum