let o, p, q, r be Point of (TOP-REAL 3); :: thesis: ( o,p,(o <X> p) <X> (q <X> r) are_LinDep & q,r,(o <X> p) <X> (q <X> r) are_LinDep )
( |{o,p,((o <X> p) <X> (q <X> r))}| = 0 & |{q,r,((o <X> p) <X> (q <X> r))}| = 0 ) by Th40;
hence ( o,p,(o <X> p) <X> (q <X> r) are_LinDep & q,r,(o <X> p) <X> (q <X> r) are_LinDep ) by Th37; :: thesis: verum