:: deftheorem defines ECIW-signature AOFA_000:def 26 :
ECIW-signature = <*0,2*> ^ <*3,2*>;