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 a9 = a as positive expression of C, an_Adj C ;
A1: ex b being positive expression of C, an_Adj C st
( Non a9 = (non_op C) term b & Non (Non a9) = b ) by Th61;
Non a9 = (non_op C) term a by Th59;
hence Non (Non a) = a by A1, Th44; :: thesis: verum

end;

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

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

end;

end;