set X = MSVars C;
consider m, a being OperSymbol of C such that
A1: ( 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;
A3: root-tree [m,the carrier of C] in the Sorts of (Free C,(MSVars C)) . a_Type by A1, MSAFREE3:6;
A4: root-tree [a,the carrier of C] in the Sorts of (Free C,(MSVars C)) . an_Adj by A2, MSAFREE3:6;
consider x being variable;
( a_Term C = a_Term & (MSVars C) . a_Term = Vars ) by MSVARS;
then A5: root-tree [x,a_Term ] in the Sorts of (Free C,(MSVars C)) . a_Term by MSAFREE3:5;
assume not the Sorts of (Free C,(MSVars C)) is non-empty ; :: according to MSUALG_1:def 8 :: thesis: contradiction
then {} in rng the Sorts of (Free C,(MSVars C)) by RELAT_1:def 9;
then consider s being set such that
A6: ( s in dom the Sorts of (Free C,(MSVars C)) & {} = the Sorts of (Free C,(MSVars C)) . s ) by FUNCT_1:def 5;
s in the carrier of C by A6, PARTFUN1:def 4;
then s in {a_Type ,an_Adj ,a_Term } by CONSTRSIGN;
hence contradiction by A3, A4, A5, A6, ENUMSET1:def 1; :: thesis: verum