theorem Th3: :: FDIFF_7:3

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