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
consider a' being expression of C, an_Adj C such that
A1: ( a = (non_op C) term a' & Non a = a' ) by Th45g;
thus (non_op C) term (Non a) = a by A1; :: thesis: verum