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