for D being non empty set
for CR, r1, r2, f being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 holds
( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )