consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj and
the_arity_of a = {} by Def12;
ex t being expression of C, a_Type C st
( t = root-tree [m, the carrier of C] & t is pure ) by A1, A2, Th70;
hence ex b₁ being expression of C, a_Type C st b₁ is pure ; :: thesis: verum