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
X: p,q _|_ r,r1 and
A2: 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,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y ) by A2, Th31, X;
then ( v - u,v1 - w1 are_Ort_wrt w,y & v - u,v2 - w1 are_Ort_wrt w,y ) by Def3;
then A3: v - u,(v2 - w1) - (v1 - w1) are_Ort_wrt w,y by A1, Th14;
(v2 - w1) - (v1 - w1) = v2 - ((v1 - w1) + w1) by RLVECT_1:41
.= v2 - (v1 - (w1 - w1)) by RLVECT_1:43
.= v2 - (v1 - (0. V)) by RLVECT_1:28
.= v2 - v1 by RLVECT_1:26 ;
then u,v,v1,v2 are_Ort_wrt w,y by A3, Def3;
hence p,q _|_ r1,r2 by Th31; :: thesis: verum