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 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 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)); ( 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
; ( 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
; q,q1 _|_ r,r1
b <> 0
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; verum