for x being set
for S being ManySortedSign holds SingleMSS x tolerates S by PARTFUN1:59;