set C = MaxConstrSign ;
set m = non_op MaxConstrSign ;
let a be quasi-adjective; :: thesis: main-constr ((non_op MaxConstrSign ) term a) = non_op
A1: len (the_arity_of (non_op MaxConstrSign )) = 1 by Udef;
the_arity_of (non_op MaxConstrSign ) = <*an_Adj *> by ABCMIZ_1:38;
then (the_arity_of (non_op MaxConstrSign )) . 1 = an_Adj MaxConstrSign by FINSEQ_1:57;
then A0: (non_op MaxConstrSign ) term a = [(non_op MaxConstrSign ),the carrier of MaxConstrSign ] -tree <*a*> by A1, ABCMIZ_1:def 30;
thus main-constr ((non_op MaxConstrSign ) term a) = (((non_op MaxConstrSign ) term a) . {} ) `1 by MCON
.= [(non_op MaxConstrSign ),the carrier of MaxConstrSign ] `1 by A0, TREES_4:def 4
.= non_op by MCART_1:7 ; :: thesis: verum