theorem :: PUA2MSS1:31

for A being partial non-empty UAStr
for P being a_partition of A holds A can_be_characterized_by MSSign (A,P)