for th1, th2 being Real st th1 in ].0,1.[ & th2 in ].0,1.[ & tan . th1 = tan . th2 holds
th1 = th2