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