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