:: deftheorem Def8 defines gate`1=arity CIRCCOMB:def 8 :
for IT being ManySortedSign holds
( IT is gate`1=arity iff for g being set st g in the carrier' of IT holds
g = [( the Arity of IT . g),(g `2)] );