theorem Th39: :: BKMODEL4:45

for a, b, c, d, e, f, r being Real st ((1 - r) * |[a,b,1]|) + (r * |[c,d,1]|) = |[e,f,1]| holds
((1 - r) * |[a,b]|) + (r * |[c,d]|) = |[e,f]|