:: deftheorem defines variables_in ABCMIZ_1:def 48 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds variables_in T = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));