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