:: deftheorem defines can_be_characterized_by PUA2MSS1:def 16 :
for A being partial non-empty UAStr
for S being non empty non void ManySortedSign holds
( A can_be_characterized_by S iff ex G being MSAlgebra over S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P );