let x, y be real number ; :: thesis: ( 0 <= x & 0 <= y & x ^2 = y ^2 implies x = y )
assume A1: ( 0 <= x & 0 <= y ) ; :: thesis: ( not x ^2 = y ^2 or x = y )
assume x ^2 = y ^2 ; :: thesis: x = y
then ( x <= y & y <= x ) by A1, Th78;
hence x = y by XXREAL_0:1; :: thesis: verum