assume - a is integer ; :: thesis: contradiction
then (- 1) * (- a) is integer ;
hence contradiction ; :: thesis: verum