len (lower_volume f,D) = len D by Def8;
hence lower_volume f,D is non empty FinSequence of REAL ; :: thesis: verum