theorem Th17: :: SQUARE_1:17

sqrt 0 = 0