let x, y be Real; :: thesis: ( 0 <= x & 0 <= y & sqrt x = sqrt y implies x = y )
assume that
A1: 0 <= x and
A2: 0 <= y and
A3: sqrt x = sqrt y ; :: thesis: x = y
assume x <> y ; :: thesis: contradiction
then ( x < y or y < x ) by XXREAL_0:1;
hence contradiction by A1, A2, A3, Lm3; :: thesis: verum