let D be non empty set ; :: thesis: for f, CR, r being File of D st r is_a_record_of f,CR holds
r is_a_record_of r,CR
let f, CR, r be File of D; :: thesis: ( r is_a_record_of f,CR implies r is_a_record_of r,CR )
assume r is_a_record_of f,CR ; :: thesis: r is_a_record_of r,CR
then A1: r is_terminated_by CR by Def1;
then addcr (r,CR) is_preposition_of by Th29;
hence r is_a_record_of r,CR by A1, Def1; :: thesis: verum