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

suppose a is positive ; :: thesis: a at f is quasi-adjective of C

then reconsider a = a as positive quasi-adjective of C ;
a at f is positive ;
hence a at f is quasi-adjective of C ; :: thesis: verum

end;

suppose a is negative ; :: thesis: a at f is quasi-adjective of C

then reconsider a = a as negative quasi-adjective of C ;
a at f is negative ;
hence a at f is quasi-adjective of C ; :: thesis: verum

end;

end;