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

suppose a is positive ; :: thesis: Non a is regular

then reconsider a9 = a as positive expression of C, an_Adj C ;
Non a9 is negative ;
hence Non a is regular ; :: thesis: verum

end;

suppose a is negative ; :: thesis: Non a is regular

then reconsider a9 = a as negative expression of C, an_Adj C ;
Non a9 is positive ;
hence Non a is regular ; :: thesis: verum

end;

end;