for o, p, q, r being Point of (TOP-REAL 3) holds
( o,p,(o <X> p) <X> (q <X> r) are_LinDep & q,r,(o <X> p) <X> (q <X> r) are_LinDep )