theorem Th1: :: GTARSKI2:1

for r, s, t, u being Real st s <> 0 & t <> 0 & r ^2 = ((s ^2) + (t ^2)) - (((2 * s) * t) * u) holds
u = (((r ^2) - (s ^2)) - (t ^2)) / (- ((2 * s) * t))