for a, b, c, d being Real st (a ^2) + (b ^2) = 1 & (c ^2) + (d ^2) = 1 & (c * a) + (d * b) = 1 holds
b * c = a * d