let x, y be Real; :: thesis: ( 0 <= x & 0 <= y & x ^2 = y ^2 implies x = y )
assume that
A1: 0 <= x and
A2: 0 <= y ; :: thesis: ( not x ^2 = y ^2 or x = y )
assume A3: x ^2 = y ^2 ; :: thesis: x = y
then A4: y <= x by A1, Th16;
x <= y by A2, A3, Th16;
hence x = y by A4, XXREAL_0:1; :: thesis: verum