for r being Real st PI / 2 <= r & r <= PI & r / PI is rational & sin r is rational holds
r in {(PI / 2),((5 * PI) / 6),PI}