theorem :: BKMODEL1:17

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