:: deftheorem defines constrs ABCMIZ_A:def 8 :
for C being initialized ConstructorSignature
for e being expression of C holds constrs e = (proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ;