let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace V,w,y) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
let w, y be VECTOR of V; :: thesis: for p, q, p1, q1 being Element of (AMSpace V,w,y) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
let p, q, p1, q1 be Element of (AMSpace V,w,y); :: thesis: ( p,q _|_ p1,q1 implies p,q _|_ q1,p1 )
assume A1: p,q _|_ p1,q1 ; :: thesis: p,q _|_ q1,p1
reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V ;
u,v,u1,v1 are_Ort_wrt w,y by A1, Th31;
then v - u,v1 - u1 are_Ort_wrt w,y by Def3;
then A2: v - u,(- 1) * (v1 - u1) are_Ort_wrt w,y by Th11;
(- 1) * (v1 - u1) = - (v1 - u1) by RLVECT_1:29
.= u1 - v1 by RLVECT_1:47 ;
then u,v,v1,u1 are_Ort_wrt w,y by A2, Def3;
hence p,q _|_ q1,p1 by Th31; :: thesis: verum