set C = MaxConstrSign ;
set m = ast MaxConstrSign;
let q be expression of MaxConstrSign , a_Type MaxConstrSign; :: thesis: for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *
let a be quasi-adjective; :: thesis: main-constr ((ast MaxConstrSign) term (a,q)) = *
A1: len (the_arity_of (ast MaxConstrSign)) = 2 by Bdef;
the_arity_of (ast MaxConstrSign) = <*(an_Adj MaxConstrSign),(a_Type MaxConstrSign)*> by ABCMIZ_1:38;
then ( (the_arity_of (ast MaxConstrSign)) . 1 = an_Adj MaxConstrSign & (the_arity_of (ast MaxConstrSign)) . 2 = a_Type MaxConstrSign ) by FINSEQ_1:61;
then A0: (ast MaxConstrSign) term (a,q) = [(ast MaxConstrSign), the carrier of MaxConstrSign] -tree <*a,q*> by A1, ABCMIZ_1:def 31;
thus main-constr ((ast MaxConstrSign) term (a,q)) = (((ast MaxConstrSign) term (a,q)) . {}) `1 by MCON
.= [(ast MaxConstrSign), the carrier of MaxConstrSign] `1 by A0, TREES_4:def 4
.= * by MCART_1:7 ; :: thesis: verum