let C be initialized ConstructorSignature; :: thesis: for a being positive expression of C, an_Adj C holds Non a = (non_op C) term a
let a be positive expression of C, an_Adj C; :: thesis: Non a = (non_op C) term a
for a' being expression of C, an_Adj C holds not a = (non_op C) term a' by POSITIVE;
hence Non a = (non_op C) term a by NON'OPA; :: thesis: verum