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