consider m, a being OperSymbol of C such that
the_result_sort_of m = a_Type and
the_arity_of m = {} and
A1: the_result_sort_of a = an_Adj and
A2: the_arity_of a = {} by Def12;
set X = MSVars C;
root-tree [a, the carrier of C] in the Sorts of (Free (C,(MSVars C))) . an_Adj by A1, A2, MSAFREE3:5;
then reconsider v = root-tree [a, the carrier of C] as expression of C, an_Adj C by Th41;
take v ; :: thesis: v is positive
given a9 being expression of C, an_Adj C such that A3: v = (non_op C) term a9 ; :: according to ABCMIZ_1:def 37 :: thesis: contradiction
v = [non_op, the carrier of C] -tree <*a9*> by A3, Th43;
then [non_op, the carrier of C] = v . {} by TREES_4:def 4
.= [a, the carrier of C] by TREES_4:3 ;
then a = non_op C by XTUPLE_0:1;
hence contradiction by A2, Def9; :: thesis: verum