theorem :: EUCLID_5:22

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