let C be initialized standardized ConstructorSignature; :: thesis: for a being expression of C holds
( a is positive quasi-adjective of C iff ( (a . {} ) `1 in Constructors & ((a . {} ) `1 ) `1 = an_Adj ) )
set X = MSVars C;
set V = (MSVars C) \/ (the carrier of C --> {0 });
let t be expression of C; :: thesis: ( t is positive quasi-adjective of C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = an_Adj ) )
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 2;
the Sorts of (Free C,(MSVars C)) is MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by A1, MSUALG_2:def 10;
then the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by PBOOLE:def 23;
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) by PBOOLE:def 5;

per cases ( ( (t . {} ) `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 Th50;

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

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

end;

suppose that B1: (t . {} ) `2 = the carrier of C and
B2: (t . {} ) `1 in Constructors and
B3: (t . {} ) `1 in the carrier' of C ; :: thesis: ( t is positive quasi-adjective of C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = an_Adj ) )

reconsider o = (t . {} ) `1 as OperSymbol of C by B3;
reconsider tt = t as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
not o in {* ,non_op } by B2, ABCMIZ_1:39, XBOOLE_0:3;
then ( o <> * & o <> non_op ) by TARSKI:def 2;
then o is constructor by ABCMIZ_1:def 11;
then B4: o `1 = the_result_sort_of o by StandardizedDef;
B7: t . {} = [o,((t . {} ) `2 )] by Lem5;
then B5: the_sort_of tt = the_result_sort_of o by B1, MSATERM:17;

hereby :: thesis: ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = an_Adj implies t is positive quasi-adjective of C )

assume t is positive quasi-adjective of C ; :: thesis: ( (t . {} ) `1 in Constructors & not ((t . {} ) `1 ) `1 <> an_Adj )
then B6: t in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by ABCMIZ_1:def 28;
thus (t . {} ) `1 in Constructors by B2; :: thesis: not ((t . {} ) `1 ) `1 <> an_Adj
assume ((t . {} ) `1 ) `1 <> an_Adj ; :: thesis: contradiction
hence contradiction by A2, B6, B4, B5, MSAFREE3:8; :: thesis: verum

end;

assume (t . {} ) `1 in Constructors ; :: thesis: ( not ((t . {} ) `1 ) `1 = an_Adj or t is positive quasi-adjective of C )
assume ((t . {} ) `1 ) `1 = an_Adj ; :: thesis: t is positive quasi-adjective of C
then reconsider t = t as expression of C, an_Adj C by B1, B4, B7, Th46;
t is positive

proof

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

end;

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

end;

suppose Z0: (t . {} ) `1 = * ; :: thesis: ( t is positive quasi-adjective of C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = an_Adj ) )

then (t . {} ) `1 in {* ,non_op } by TARSKI:def 2;
then Z2: not (t . {} ) `1 in Constructors by XBOOLE_0:3, ABCMIZ_1:39;
consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that
Z1: t = [* ,3] -tree a,q by Z0, Th52;
t = [* ,3] -tree <*a,q*> by Z1, TREES_4:def 6;
then t . {} = [* ,3] by TREES_4:def 4;
then (t . {} ) `1 = * by MCART_1:7;
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 Th47;
hence ( t is positive quasi-adjective of C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = an_Adj ) ) by Z2, ABCMIZ_1:48; :: thesis: verum

end;

suppose Z0: (t . {} ) `1 = non_op ; :: thesis: ( t is positive quasi-adjective of C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = an_Adj ) )

then (t . {} ) `1 in {* ,non_op } by TARSKI:def 2;
then Z2: not (t . {} ) `1 in Constructors by XBOOLE_0:3, ABCMIZ_1:39;
consider a being expression of C, an_Adj C such that
Z1: t = [non_op ,3] -tree a by Z0, Th53;
t = [non_op ,3] -tree <*a*> by Z1, 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 Z2, ABCMIZ_1:def 37; :: thesis: verum

end;

end;