ex a9 being positive expression of C, an_Adj C st
( a = (non_op C) term a9 & Non a = a9 ) by Th61;
hence Non a is positive ; :: thesis: verum