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;