theorem :: FACIRC_2:3

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