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;