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