theorem Th2: :: FDIFF_7:2

for x being Real st x > 0 holds
x #R (1 / 2) = sqrt x