consider m, a being OperSymbol of C such that
( the_result_sort_of m = a_Type & the_arity_of m = {} ) and
A2: ( the_result_sort_of a = an_Adj & the_arity_of a = {} ) by INITIALIZED;
set X = MSVars C;
( root-tree [a,the carrier of C] in the Sorts of (Free C,(MSVars C)) . an_Adj & an_Adj C = an_Adj ) by A2, MSAFREE3:6;
then reconsider v = root-tree [a,the carrier of C] as expression of C, an_Adj C by Th42;
take v ; :: thesis: v is positive
given a' being expression of C, an_Adj C such that A1: v = (non_op C) term a' ; :: according to ABCMIZ_1:def 37 :: thesis: contradiction
v = [non_op ,the carrier of C] -tree <*a'*> by A1, ThNon;
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 ZFMISC_1:33;
hence contradiction by A2, CONSTRSIGN; :: thesis: verum