for x, y, z being Real holds |[0,0,0]| <X> |[x,y,z]| = 0. (TOP-REAL 3)