:: deftheorem defines vars ABCMIZ_1:def 47 :
for C being initialized ConstructorSignature
for e being expression of C holds vars e = varcl (variables_in e);