theorem :: BKMODEL1:20

for a, b, c, d being Real
for u, v, w being Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
|{u,v,w}| = 0