theorem Th09: :: BKMODEL3:8

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