theorem Th28: :: SQUARE_1:28

for x, y being Real st 0 <= x & 0 <= y & sqrt x = sqrt y holds
x = y