set X = MSVars C;
consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
A3: the_result_sort_of a = an_Adj and
A4: the_arity_of a = {} by Def12;
A5: root-tree [m,the carrier of C] in the Sorts of (Free C,(MSVars C)) . a_Type by A1, A2, MSAFREE3:6;
A6: root-tree [a,the carrier of C] in the Sorts of (Free C,(MSVars C)) . an_Adj by A3, A4, MSAFREE3:6;
consider x being variable;
A7: a_Term C = a_Term ;
(MSVars C) . a_Term = Vars by Def25;
then A8: root-tree [x,a_Term ] in the Sorts of (Free C,(MSVars C)) . a_Term by A7, 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
A9: s in dom the Sorts of (Free C,(MSVars C)) and
A10: {} = the Sorts of (Free C,(MSVars C)) . s by FUNCT_1:def 5;
s in the carrier of C by A9, PARTFUN1:def 4;
then s in {a_Type ,an_Adj ,a_Term } by Def9;
hence contradiction by A5, A6, A8, A10, ENUMSET1:def 1; :: thesis: verum