theorem :: ABCMIZ_1:68

for C being initialized ConstructorSignature
for a1, a2 being quasi-adjective of C st Non a1 = Non a2 holds
a1 = a2