set C = MaxConstrSign ;
set m = [a_Type ,[{} ,0 ]];
set a = [an_Adj ,[{} ,0 ]];
set f = [a_Term ,[{} ,0 ]];
( a_Type in {a_Type } & an_Adj in {an_Adj } & a_Term in {a_Term } & [(<*> Vars ),0 ] in [:QuasiLoci ,NAT :] ) by Th31, TARSKI:def 1, ZFMISC_1:def 2;
then A0: ( [a_Type ,[{} ,0 ]] in Modes & [an_Adj ,[{} ,0 ]] in Attrs & [a_Term ,[{} ,0 ]] in Funcs ) by ZFMISC_1:def 2;
then ( [a_Type ,[{} ,0 ]] in Modes \/ Attrs & [an_Adj ,[{} ,0 ]] in Modes \/ Attrs ) by XBOOLE_0:def 3;
then ( [a_Type ,[{} ,0 ]] in Constructors & [an_Adj ,[{} ,0 ]] in Constructors & [a_Term ,[{} ,0 ]] in Constructors & the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors ) by A0, MAXdef, XBOOLE_0:def 3;
then reconsider m = [a_Type ,[{} ,0 ]], a = [an_Adj ,[{} ,0 ]], f = [a_Term ,[{} ,0 ]] as OperSymbol of MaxConstrSign by XBOOLE_0:def 3;
( m is constructor & a is constructor & f is constructor ) by CNSTR2;
then ( the ResultSort of MaxConstrSign . m = m `1 & the ResultSort of MaxConstrSign . a = a `1 & the ResultSort of MaxConstrSign . f = f `1 ) by MAXdef;
then A1: ( the ResultSort of MaxConstrSign . m = a_Type & the ResultSort of MaxConstrSign . a = an_Adj & the ResultSort of MaxConstrSign . f = a_Term ) by MCART_1:7;
A2: the carrier of MaxConstrSign = {a_Type ,an_Adj ,a_Term } by CONSTRSIGN;
let x be set ; :: according to TARSKI:def 3,ABCMIZ_1:def 54 :: thesis: ( not x in the carrier of MaxConstrSign or x in rng the ResultSort of MaxConstrSign )
assume x in the carrier of MaxConstrSign ; :: thesis: x in rng the ResultSort of MaxConstrSign
then ( x = a_Type or x = an_Adj or x = a_Term ) by A2, ENUMSET1:def 1;
hence x in rng the ResultSort of MaxConstrSign by A1, FUNCT_2:6; :: thesis: verum