a = (sqrt (O,a)) ^2 by defq;
hence not sqrt (O,a) is zero ; :: thesis: verum