theorem Th37: :: COMPTRIG:37

for x being Real st x > 0 holds
Arg (x * <i>) = PI / 2