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