for o, p, q, r being Point of (TOP-REAL 3) holds
( |{o,p,((o <X> p) <X> (q <X> r))}| = 0 & |{q,r,((o <X> p) <X> (q <X> r))}| = 0 )