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