reconsider r = ( the InternalRel of R `) \ (id the carrier of R) as Relation of the carrier of R ;
take RelStr(# the carrier of R,r #) ; :: thesis: ( the carrier of RelStr(# the carrier of R,r #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,r #) = ( the InternalRel of R `) \ (id the carrier of R) )
thus ( the carrier of RelStr(# the carrier of R,r #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,r #) = ( the InternalRel of R `) \ (id the carrier of R) ) ; :: thesis: verum