assume SpStSeq D is constant ; :: thesis: contradiction
then <*(SW-corner D),(NW-corner D)*> is constant by Th1;
then |[(W-bound D),(N-bound D)]| = |[(W-bound D),(S-bound D)]| by Th2;
then N-bound D = S-bound D by SPPOL_2:1;
hence contradiction by Th16; :: thesis: verum