let D be non empty set ; :: thesis: for r, CR being File of D st CR is_postposition_of r holds
0 <= (len r) - (len CR)
let f, g be File of D; :: thesis: ( g is_postposition_of f implies 0 <= (len f) - (len g) )
assume g is_postposition_of f ; :: thesis: 0 <= (len f) - (len g)
then len g <= len f by FINSEQ_8:23;
then (len g) - (len g) <= (len f) - (len g) by XREAL_1:9;
hence 0 <= (len f) - (len g) ; :: thesis: verum