:: deftheorem defines Output CIRCCMB3:def 8 :
for S being one-gate ManySortedSign holds Output S = union the carrier' of S;