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