let D be non empty set ; :: thesis: for CR, r being File of D holds addcr (r,CR) = (ovlldiff (r,CR)) ^ CR
let CR, r be File of D; :: thesis: addcr (r,CR) = (ovlldiff (r,CR)) ^ CR
addcr (r,CR) = ovlcon (r,CR) by FINSEQ_8:def 11
.= (ovlldiff (r,CR)) ^ ((ovlpart (r,CR)) ^ (ovlrdiff (r,CR))) by FINSEQ_8:12
.= (ovlldiff (r,CR)) ^ CR by Th32 ;
hence addcr (r,CR) = (ovlldiff (r,CR)) ^ CR ; :: thesis: verum