consider m, a being OperSymbol of C such that
( the_result_sort_of m = a_Type & the_arity_of m = {} ) and
A1: ( the_result_sort_of a = an_Adj & the_arity_of a = {} ) by INITIALIZED;
consider mm being expression of C, an_Adj C such that
A5: ( mm = root-tree [a,the carrier of C] & mm is positive ) by A1, ThP2;
reconsider mm = mm as quasi-adjective of C by A5;
take mm ; :: thesis: mm is ground
set p = <*> (Union the Sorts of (Free C,(MSVars C)));
A2: mm = [a,the carrier of C] -tree (<*> (Union the Sorts of (Free C,(MSVars C)))) by A5, TREES_4:20;
( a <> * & a <> non_op ) by A1, CONSTRSIGN;
then A3: a is constructor by CNSTR2;
variables_in mm c= {}

proof

let x be set ; :: 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 A2, A3, Th84;
then consider Y being set such that
A4: ( x in Y & 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 A4;
hence x in {} ; :: thesis: verum

end;

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