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