theorem :: SIN_COS6:75
for r being Real st - 1 <= r & r <= 1 & arcsin r = PI / 2 holds
r = 1 by Th68, SIN_COS:77;