:: deftheorem Def58 defines irrelevant ABCMIZ_1:def 58 :
for C being initialized ConstructorSignature
for f being valuation of C holds
( f is irrelevant iff for x being variable st x in dom f holds
ex y being variable st f . x = y -term C );