for D being non empty set
for r, CR being File of D st CR is_postposition_of r holds
0 <= (len r) - (len CR)