assume not 2 -root a is even ; :: thesis: contradiction
then (2 -root a) |^ 2 is odd ;
hence contradiction ; :: thesis: verum