theorem :: ABCMIZ_A:34

for x being variable
for C being initialized ConstructorSignature holds main-constr (x -term C) = {} by Def9;