theorem :: FILEREC1:33

for D being non empty set
for CR, r being File of D holds addcr (r,CR) = (ovlldiff (r,CR)) ^ CR