:: deftheorem defines -term ABCMIZ_1:def 34 :
for x being variable
for C being initialized ConstructorSignature holds x -term C = root-tree [x,a_Term];