assume SpStSeq D is constant ; :: thesis: contradiction
then <*(NW-corner D),(NE-corner D),(SE-corner D)*> is constant by Th3;
then |[(W-bound D),(N-bound D)]| = |[(E-bound D),(N-bound D)]| by Th5;
then W-bound D = E-bound D by SPPOL_2:1;
hence contradiction by Th17; :: thesis: verum