theorem :: EUCLID_5:20

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