let a be real number ; :: thesis: ( a >= 0 implies 2 -Root a = sqrt a )
assume A1: ( a >= 0 & 2 -Root a <> sqrt a ) ; :: thesis: contradiction
A2: (sqrt a) |^ 2 = (sqrt a) ^2 by NEWTON:100
.= a by A1, SQUARE_1:def 4 ;
sqrt a >= 0 by A1, SQUARE_1:def 4;
hence contradiction by A1, A2, Th28; :: thesis: verum