let x be Real; :: thesis: ( x > 0 implies x #R (- (1 / 2)) = 1 / (sqrt x) )
assume A1: x > 0 ; :: thesis: x #R (- (1 / 2)) = 1 / (sqrt x)
hence x #R (- (1 / 2)) = 1 / (x #R (1 / 2)) by PREPOWER:76
.= 1 / (sqrt x) by A1, Th2 ;
:: thesis: verum