let C be initialized ConstructorSignature; :: thesis: for a being quasi-adjective of C holds Non (Non a) = a
let a be quasi-adjective of C; :: thesis: Non (Non a) = a

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

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

then reconsider a' = a as positive expression of C, an_Adj C ;
consider b being positive expression of C, an_Adj C such that
A1: ( Non a' = (non_op C) term b & Non (Non a') = b ) by Th45;
Non a' = (non_op C) term a by Th44;
hence Non (Non a) = a by A1, ThNon'; :: thesis: verum

end;

suppose a is negative ; :: thesis: Non (Non a) = a

then reconsider a' = a as negative expression of C, an_Adj C ;
ex b being positive expression of C, an_Adj C st
( a' = (non_op C) term b & Non a' = b ) by Th45;
hence Non (Non a) = a by Th44; :: thesis: verum

end;

end;