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 a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 by Def37;
hence Non a = (non_op C) term a by Def36; :: thesis: verum