:: deftheorem defines gate`2=den CIRCCOMB:def 10 :
for S being non empty ManySortedSign
for IT being MSAlgebra over S holds
( IT is gate`2=den iff for g being set st g in the carrier' of S holds
g = [(g `1),( the Charact of IT . g)] );