let a be Real; :: thesis: ( a >= 0 implies 2 -Root a = sqrt a )
assume that
A1: a >= 0 and
A2: 2 -Root a <> sqrt a ; :: thesis: contradiction
A3: sqrt a >= 0 by A1, SQUARE_1:def 2;
(sqrt a) |^ 2 = (sqrt a) ^2 by NEWTON:81
.= a by A1, SQUARE_1:def 2 ;
hence contradiction by A2, A3, Th19; :: thesis: verum