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