smid (p,m,n) = (p /^ (m -' 1)) | ((n + 1) -' m) by FINSEQ_8:def 1;
hence smid (p,m,n) is non-Dmulti ; :: thesis: verum