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 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 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: ( p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 implies q,q1 _|_ r,r1 )
assume that
A1: p,p1 _|_ q,q1 and
A2: 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 ;
consider a, b being Real such that
A3: a * (v - u) = b * (v2 - u2) and
A4: ( a <> 0 or b <> 0 ) by A2, Th22;
assume A5: p <> p1 ; :: thesis: q,q1 _|_ r,r1
b <> 0

proof

assume A6: b = 0 ; :: thesis: contradiction
then a * (v - u) = 0. V by A3, RLVECT_1:10;
then v - u = 0. V by A4, A6, RLVECT_1:11;
hence contradiction by A5, RLVECT_1:21; :: thesis: verum

end;

then A7: v2 - u2 = (b ") * (a * (v - u)) by A3, ANALOAF:5
.= ((b ") * a) * (v - u) by RLVECT_1:def 7 ;
u,v,u1,v1 are_Ort_wrt w,y by A1, Th21;
then v - u,v1 - u1 are_Ort_wrt w,y ;
then v2 - u2,v1 - u1 are_Ort_wrt w,y by A7, Th7;
then v1 - u1,v2 - u2 are_Ort_wrt w,y ;
then u1,v1,u2,v2 are_Ort_wrt w,y ;
hence q,q1 _|_ r,r1 by Th21; :: thesis: verum