set C = MaxConstrSign ;
set m = [a_Type ,[{} ,0 ]];
set a = [an_Adj ,[{} ,0 ]];
set f = [a_Term ,[{} ,0 ]];
A1:
a_Type in {a_Type }
by TARSKI:def 1;
A2:
an_Adj in {an_Adj }
by TARSKI:def 1;
A3:
a_Term in {a_Term }
by TARSKI:def 1;
A4:
[(<*> Vars ),0 ] in [:QuasiLoci ,NAT :]
by Th29, ZFMISC_1:def 2;
then A5:
[a_Type ,[{} ,0 ]] in Modes
by A1, ZFMISC_1:def 2;
A6:
[an_Adj ,[{} ,0 ]] in Attrs
by A2, A4, ZFMISC_1:def 2;
A7:
[a_Term ,[{} ,0 ]] in Funcs
by A3, A4, ZFMISC_1:def 2;
A8:
[a_Type ,[{} ,0 ]] in Modes \/ Attrs
by A5, XBOOLE_0:def 3;
A9:
[an_Adj ,[{} ,0 ]] in Modes \/ Attrs
by A6, XBOOLE_0:def 3;
A10:
[a_Type ,[{} ,0 ]] in Constructors
by A8, XBOOLE_0:def 3;
A11:
[an_Adj ,[{} ,0 ]] in Constructors
by A9, XBOOLE_0:def 3;
A12:
[a_Term ,[{} ,0 ]] in Constructors
by A7, XBOOLE_0:def 3;
the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors
by Def24;
then reconsider m = [a_Type ,[{} ,0 ]], a = [an_Adj ,[{} ,0 ]], f = [a_Term ,[{} ,0 ]] as OperSymbol of MaxConstrSign by A10, A11, A12, XBOOLE_0:def 3;
A13:
m is constructor
by Def11;
A14:
a is constructor
by Def11;
A15:
f is constructor
by Def11;
A16:
the ResultSort of MaxConstrSign . m = m `1
by A13, Def24;
A17:
the ResultSort of MaxConstrSign . a = a `1
by A14, Def24;
A18:
the ResultSort of MaxConstrSign . f = f `1
by A15, Def24;
A19:
the ResultSort of MaxConstrSign . m = a_Type
by A16, MCART_1:7;
A20:
the ResultSort of MaxConstrSign . a = an_Adj
by A17, MCART_1:7;
A21:
the ResultSort of MaxConstrSign . f = a_Term
by A18, MCART_1:7;
A22:
the carrier of MaxConstrSign = {a_Type ,an_Adj ,a_Term }
by Def9;
let x be set ; TARSKI:def 3,ABCMIZ_1:def 54 ( not x in the carrier of MaxConstrSign or x in rng the ResultSort of MaxConstrSign )
assume
x in the carrier of MaxConstrSign
; x in rng the ResultSort of MaxConstrSign
then
( x = a_Type or x = an_Adj or x = a_Term )
by A22, ENUMSET1:def 1;
hence
x in rng the ResultSort of MaxConstrSign
by A19, A20, A21, FUNCT_2:6; verum