let r, s be Real; :: thesis: ( 0 <= r & 0 <= s & r ^2 = s ^2 implies r = s )
assume that
A1: 0 <= r and
A2: 0 <= s and
A3: r ^2 = s ^2 and
A4: r <> s ; :: thesis: contradiction
- Q >= - (- s) by A1, A3, A4, SQUARE_1:40;
hence contradiction by A4, A2, A3, SQUARE_1:40; :: thesis: verum