let D be non empty set ; :: thesis: for f, CR being File of D holds CR is_substring_of addcr (f,CR),1
let f, CR be File of D; :: thesis: 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; :: thesis: verum