consider m, a being OperSymbol of C such that
the_result_sort_of m = a_Type and
the_arity_of m = {} and
A7: the_result_sort_of a = an_Adj and
A8: the_arity_of a = {} by Def12;
consider mm being expression of C, an_Adj C such that
A9: mm = root-tree [a, the carrier of C] and
A10: mm is positive by A7, A8, Th71;
reconsider mm = mm as quasi-adjective of C by A10;
take mm ; :: thesis: mm is ground
set p = <*> (Union the Sorts of (Free (C,(MSVars C))));
A11: mm = [a, the carrier of C] -tree (<*> (Union the Sorts of (Free (C,(MSVars C))))) by A9, TREES_4:20;
A12: a <> * by A7, Def9;
a <> non_op by A8, Def9;
then A13: a is constructor by A12;
variables_in mm c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in variables_in mm or x in {} )
assume x in variables_in mm ; :: thesis: x in {}
then x in union { (variables_in t) where t is quasi-term of C : t in rng (<*> (Union the Sorts of (Free (C,(MSVars C))))) } by A11, A13, Th88;
then consider Y being set such that
x in Y and
A14: Y in { (variables_in t) where t is quasi-term of C : t in rng (<*> (Union the Sorts of (Free (C,(MSVars C))))) } by TARSKI:def 4;
ex t being quasi-term of C st
( Y = variables_in t & t in rng (<*> (Union the Sorts of (Free (C,(MSVars C))))) ) by A14;
hence x in {} ; :: thesis: verum

end;

then variables_in mm = {} ;
hence mm is ground by Th107; :: thesis: verum