let C be initialized standardized ConstructorSignature; :: thesis:
set X = MSVars C;
set V = (MSVars C) (\/) ( the carrier of C --> {0});
let t be expression of C; :: thesis:
consider A being MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) such that
A1: ( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) (\/) ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def 1;
the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by A1, MSUALG_2:def 9;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by PBOOLE:def 18;
then A2: the Sorts of (Free (C,(MSVars C))) . (an_Adj C) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (an_Adj C) ;

per cases ) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) or ( (t . {}) `2 = the carrier of C & (t . {}) `1 in Constructors & (t . {}) `1 in the carrier' of C ) or (t . {}) `1 = * or (t . {}) `1 = non_op ) by Th14;

suppose ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) ; :: thesis:

hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by Th8, ABCMIZ_1:77, XBOOLE_0:3; :: thesis:

end;

suppose that A3: (t . {}) `2 = the carrier of C and
A4: (t . {}) `1 in Constructors and
A5: (t . {}) `1 in the carrier' of C ; :: thesis:

reconsider o = (t . {}) `1 as OperSymbol of C by A5;
reconsider tt = t as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
not o in {*,non_op} by A4, ABCMIZ_1:39, XBOOLE_0:3;
then ( o <> * & o <> non_op ) by TARSKI:def 2;
then o is constructor ;
then A6: o `1 = the_result_sort_of o by Def1;
A7: t . {} = [o,((t . {}) `2)] ;
then A8: the_sort_of tt = the_result_sort_of o by A3, MSATERM:17;

hereby :: thesis:

assume t is positive quasi-adjective of C ; :: thesis:
then A9: t in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by ABCMIZ_1:def 28;
thus (t . {}) `1 in Constructors by A4; :: thesis:
assume ((t . {}) `1) `1 <> an_Adj ; :: thesis:
hence contradiction by A2, A9, A6, A8, MSAFREE3:7; :: thesis:

end;

assume (t . {}) `1 in Constructors ; :: thesis:
assume ((t . {}) `1) `1 = an_Adj ; :: thesis:
then reconsider t = t as expression of C, an_Adj C by A3, A6, A7, Th12;
t is positive

given a being expression of C, an_Adj C such that A10: t = (non_op C) term a ; :: according to ABCMIZ_1:def 37 :: thesis:
t = [non_op, the carrier of C] -tree <*a*> by A10, ABCMIZ_1:43;
then t . {} = [non_op, the carrier of C] by TREES_4:def 4;
then (t . {}) `1 = non_op ;
then (t . {}) `1 in {*,non_op} by TARSKI:def 2;
hence contradiction by A4, ABCMIZ_1:39, XBOOLE_0:3; :: thesis:

end;

hence t is positive quasi-adjective of C ; :: thesis:

end;

suppose A11: (t . {}) `1 = * ; :: thesis:

then (t . {}) `1 in {*,non_op} by TARSKI:def 2;
then A12: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that
A13: t = [*,3] -tree (a,q) by A11, Th18;
t = [*,3] -tree <*a,q*> by A13, TREES_4:def 6;
then t . {} = [*,3] by TREES_4:def 4;
then (t . {}) `1 = * ;
then ( t is expression of C, a_Type C & a_Type C = a_Type & a_Type = 0 & an_Adj C = an_Adj & an_Adj = 1 ) by Th13;
hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by A12, ABCMIZ_1:48; :: thesis:

end;

suppose A14: (t . {}) `1 = non_op ; :: thesis:

then (t . {}) `1 in {*,non_op} by TARSKI:def 2;
then A15: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C such that
A16: t = [non_op,3] -tree a by A14, Th19;
t = [non_op,3] -tree <*a*> by A16, TREES_4:def 5
.= [non_op, the carrier of C] -tree <*a*> by ABCMIZ_1:def 9, YELLOW11:1
.= (non_op C) term a by ABCMIZ_1:43 ;
hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by A15, ABCMIZ_1:def 37; :: thesis:

end;

end;