assume - a is rational ; :: thesis: contradiction
then reconsider b = - a as Rational ;
- b is rational ;
hence contradiction ; :: thesis: verum