let V be RealLinearSpace; 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; 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)); ( 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
; ( 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
; 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; verum