let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, q, r, r1, r2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds
p,q _|_ r1,r2
let w, y be VECTOR of V; :: thesis: for p, q, r, r1, r2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds
p,q _|_ r1,r2
let p, q, r, r1, r2 be Element of (AMSpace (V,w,y)); :: thesis: ( Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 implies p,q _|_ r1,r2 )
assume that
A1: Gen w,y and
A2: p,q _|_ r,r1 and
A3: p,q _|_ r,r2 ; :: thesis: p,q _|_ r1,r2
reconsider u = p, v = q, w1 = r, v1 = r1, v2 = r2 as Element of V ;
u,v,w1,v2 are_Ort_wrt w,y by A3, Th21;
then A4: v - u,v2 - w1 are_Ort_wrt w,y ;
A5: (v2 - w1) - (v1 - w1) = v2 - ((v1 - w1) + w1) by RLVECT_1:27
.= v2 - (v1 - (w1 - w1)) by RLVECT_1:29
.= v2 - (v1 - (0. V)) by RLVECT_1:15
.= v2 - v1 by RLVECT_1:13 ;
u,v,w1,v1 are_Ort_wrt w,y by A2, Th21;
then v - u,v1 - w1 are_Ort_wrt w,y ;
then v - u,(v2 - w1) - (v1 - w1) are_Ort_wrt w,y by A1, A4, Th10;
then u,v,v1,v2 are_Ort_wrt w,y by A5;
hence p,q _|_ r1,r2 by Th21; :: thesis: verum