let C be initialized ConstructorSignature; :: thesis: for a being expression of C, an_Adj C holds variables_in ((non_op C) term a) = variables_in a
let a be expression of C, an_Adj C; :: thesis: variables_in ((non_op C) term a) = variables_in a
(non_op C) term a = [non_op ,the carrier of C] -tree <*a*> by ThNon;
hence variables_in ((non_op C) term a) = variables_in a by Aux1; :: thesis: verum