theorem Th07: :: BKMODEL4:14

for a, b being Real
for P, Q being Element of (TOP-REAL 2) st P <> Q & ((1 - a) * P) + (a * Q) = ((1 - b) * P) + (b * Q) holds
a = b