theorem Th18: :: SQUARE_1:18

sqrt 1 = 1