theorem Th30: :: FILEREC1:30

for D being non empty set
for f, CR being File of D holds
( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR )