let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, q, p1, p2 being Element of (AMSpace V,w,y) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1
let w, y be VECTOR of V; :: thesis: for p, q, p1, p2 being Element of (AMSpace V,w,y) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1
let p, q, p1, p2 be Element of (AMSpace V,w,y); :: thesis: ( Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p implies p2,q _|_ p,p1 )
assume that
A1: Gen w,y and
X: p,q _|_ p1,p2 and
A2: p1,q _|_ p2,p ; :: thesis: p2,q _|_ p,p1
reconsider u = p, v = q, u1 = p1, u2 = p2 as Element of V ;
( u,v,u1,u2 are_Ort_wrt w,y & u1,v,u2,u are_Ort_wrt w,y ) by A2, Th31, X;
then A3: ( v - u,u2 - u1 are_Ort_wrt w,y & v - u1,u - u2 are_Ort_wrt w,y ) by Def3;

A4: now

let u, v, w be VECTOR of V; :: thesis: (u - v) - (u - w) = w - v
thus (u - v) - (u - w) = (w - u) + (u - v) by RLVECT_1:47
.= w - v by ANALOAF:4 ; :: thesis: verum

end;

then A5: (v - u1) - (v - u2) = u2 - u1 ;
A6: (v - u2) - (v - u) = u - u2 by A4;
A7: (v - u) - (v - u1) = u1 - u by A4;
v - u2,(v - u) - (v - u1) are_Ort_wrt w,y by A1, A3, A5, A6, Th16;
then u2,v,u,u1 are_Ort_wrt w,y by A7, Def3;
hence p2,q _|_ p,p1 by Th31; :: thesis: verum