theorem :: ANPROJ_8:50

for p, q, r being Point of (TOP-REAL 3) st p <X> q = 0. (TOP-REAL 3) & r = |[1,1,1]| holds
p,q,r are_LinDep