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