theorem :: FILEREC1:43

for D being non empty set
for f, CR, r being File of D st r is_a_record_of f,CR holds
r is_a_record_of r,CR by Th28;