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 ( r is_preposition_of & r is_terminated_by CR ) by Def1;
then ( addcr r,CR is_preposition_of & r is_terminated_by CR ) by Th29;
hence r is_a_record_of r,CR by Def1; :: thesis: verum