consider v being constructor OperSymbol of C such that
A1: the_result_sort_of v = an_Adj C and
A2: ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of v) & a = v -trm p ) by Th65;
consider p being FinSequence of QuasiTerms C such that
A3: len p = len (the_arity_of v) and
A4: a = v -trm p by A2;
A5: len (p at f) = len p by Th130;
a at f = v -trm (p at f) by A3, A4, Def60;
hence for b₁ being expression of C, an_Adj C st b₁ = a at f holds
b₁ is positive by A1, A3, A5, Th66; :: thesis: verum