(2 -root a) * (2 -root a) = (2 -root a) |^ 2 by NEWTON:81;
hence (2 -root a) * (2 -root a) = a ; :: thesis: verum