let D be non empty set ; for f, CR being File of D holds CR is_substring_of addcr (f,CR),1
let f, CR be File of D; CR is_substring_of addcr (f,CR),1
addcr (f,CR) = ovlcon (f,CR)
by FINSEQ_8:def 11;
hence
CR is_substring_of addcr (f,CR),1
by Th39; verum