len (lower_volume f,D) = len D by Def8;
hence not lower_volume f,D is empty ; :: thesis: verum