let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace V,w,y) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds
q,q1 // r,r1
let w, y be VECTOR of V; :: thesis: for p, p1, q, q1, r, r1 being Element of (AMSpace V,w,y) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds
q,q1 // r,r1
let p, p1, q, q1, r, r1 be Element of (AMSpace V,w,y); :: thesis: ( Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 implies q,q1 // r,r1 )
assume that
A1: Gen w,y and
X: p,p1 _|_ q,q1 and
A2: p,p1 _|_ r,r1 ; :: thesis: ( p = p1 or q,q1 // r,r1 )
assume A3: p <> p1 ; :: thesis: q,q1 // r,r1
reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V ;
( u,v,u1,v1 are_Ort_wrt w,y & u,v,u2,v2 are_Ort_wrt w,y ) by A2, Th31, X;
then A4: ( v - u,v1 - u1 are_Ort_wrt w,y & v - u,v2 - u2 are_Ort_wrt w,y ) by Def3;
v - u <> 0. V by A3, RLVECT_1:35;
then ex a, b being Real st
( a * (v1 - u1) = b * (v2 - u2) & ( a <> 0 or b <> 0 ) ) by A1, A4, Th13;
hence q,q1 // r,r1 by Th32; :: thesis: verum