for D being non empty set
for CR, r1, r2 being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR holds
CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1