:: deftheorem defines gate`2=den CIRCCOMB:def 11 :
for IT being non empty ManySortedSign holds
( IT is gate`2=den iff ex A being MSAlgebra over IT st A is gate`2=den );