theorem :: ABCMIZ_A:47

for q being expression of MaxConstrSign , a_Type MaxConstrSign
for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *