for a being Real st sin a = 0 holds
cos a <> 0