:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :
for b₁ being strict ConstructorSignature holds
( b₁ = MaxConstrSign iff ( the carrier' of b₁ = {*,non_op} \/ Constructors & ( for o being OperSymbol of b₁ st o is constructor holds
( the ResultSort of b₁ . o = o `1 & card ( the Arity of b<sub>1</sub> . o) = card ((o `2) `1) ) ) ) );