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