for u, v being Element of (TOP-REAL 3)
for a, b, c, d, e being Real st u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds
c = 0