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