let D be non empty set ; :: thesis: for f, g being File of D st f is_terminated_by g holds
len g <= len f
let f, g be File of D; :: thesis: ( f is_terminated_by g implies len g <= len f )
assume A1: f is_terminated_by g ; :: thesis: len g <= len f

per cases ( len g > 0 or len g <= 0 ) ;

suppose len g > 0 ; :: thesis: len g <= len f

hence len g <= len f by A1, FINSEQ_8:def 12; :: thesis: verum

end;

suppose len g <= 0 ; :: thesis: len g <= len f

hence len g <= len f by NAT_1:2; :: thesis: verum

end;

end;