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