let C be initialized ConstructorSignature; :: thesis: for a being non positive expression of C, an_Adj C holds (non_op C) term (Non a) = a
let a be non positive expression of C, an_Adj C; :: thesis: (non_op C) term (Non a) = a
ex a9 being expression of C, an_Adj C st
( a = (non_op C) term a9 & Non a = a9 ) by Th60;
hence (non_op C) term (Non a) = a ; :: thesis: verum