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