theorem Th08: :: BKMODEL2:15

for u, v, w being Element of (TOP-REAL 3) st v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds
|{u,v,w}| = 0