theorem Th40: :: FILEREC1:40

for D being non empty set
for f, CR being File of D holds CR is_substring_of addcr (f,CR),1