theorem Th1: :: ALGSTR_3:1

for u, u9, v, v9 being Real st u <> u9 holds
ex x being Real st (u * x) + v = (u9 * x) + v9