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
A2: p,p1 _|_ q,q1 and
A3: p,p1 _|_ r,r1 ; :: thesis: ( p = p1 or q,q1 // r,r1 )
reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V ;
u,v,u2,v2 are_Ort_wrt w,y by A3, Th21;
then A4: v - u,v2 - u2 are_Ort_wrt w,y ;
assume p <> p1 ; :: thesis: q,q1 // r,r1
then A5: v - u <> 0. V by RLVECT_1:21;
u,v,u1,v1 are_Ort_wrt w,y by A2, Th21;
then v - u,v1 - u1 are_Ort_wrt w,y ;
then ex a, b being Real st
( a * (v1 - u1) = b * (v2 - u2) & ( a <> 0 or b <> 0 ) ) by A1, A4, A5, Th9;
hence q,q1 // r,r1 by Th22; :: thesis: verum