let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, p1, p2, q 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, p1, p2, q 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, p1, p2, q 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
A2: p,q _|_ p1,p2 and
A3: 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 by A2, Th21;
then A4: v - u,u2 - u1 are_Ort_wrt w,y ;
u1,v,u2,u are_Ort_wrt w,y by A3, Th21;
then A5: v - u1,u - u2 are_Ort_wrt w,y ;

A6: now :: thesis: for u, v, w being VECTOR of V holds (u - v) - (u - w) = w - v

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:33
.= w - v by ANALOAF:1 ; :: thesis: verum

end;

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