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
; 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= {}
then
variables_in mm = {}
;
hence
mm is ground
by Th107; verum