theorem :: EUCLID_5:21

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