theorem Th03: :: BKMODEL3:3

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