:: deftheorem defines is_a_record_of FILEREC1:def 1 :
for D being non empty set
for r, f, CR being File of D holds
( r is_a_record_of f,CR iff ( ( CR ^ r is_substring_of addcr (f,CR),1 or r is_preposition_of addcr (f,CR) ) & r is_terminated_by CR ) );