let C be initialized ConstructorSignature; :: thesis: for a being expression of C, an_Adj C holds variables_in (Non a) = variables_in a
let a be expression of C, an_Adj C; :: thesis: variables_in (Non a) = variables_in a

per cases ( not a is positive or a is positive ) ;

suppose not a is positive ; :: thesis: variables_in (Non a) = variables_in a

then consider a9 being expression of C, an_Adj C such that
A1: a = (non_op C) term a9 and
A2: Non a = a9 by Th60;
[(non_op C), the carrier of C] -tree <*a9*> = a by A1, Th43;
hence variables_in (Non a) = variables_in a by A2, Th93; :: thesis: verum

end;

suppose a is positive ; :: thesis: variables_in (Non a) = variables_in a

then Non a = (non_op C) term a by Th59
.= [non_op, the carrier of C] -tree <*a*> by Th43 ;
hence variables_in (Non a) = variables_in a by Th93; :: thesis: verum

end;

end;