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

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