for S, S9 being non empty strict ManySortedSign st S <= S9 & S9 <= S holds
S = S9