let V be RealLinearSpace; :: thesis: for w, y being VECTOR of
for p, q, p1, q1 being Element of st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
let w, y be VECTOR of ; :: thesis: for p, q, p1, q1 being Element of st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
let p, q, p1, q1 be Element of ; :: thesis: ( p,q _|_ p1,q1 implies p1,q1 _|_ p,q )
reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of ;
assume p,q _|_ p1,q1 ; :: thesis: p1,q1 _|_ p,q
then u,v,u1,v1 are_Ort_wrt w,y by Th31;
then v - u,v1 - u1 are_Ort_wrt w,y by Def3;
then v1 - u1,v - u are_Ort_wrt w,y by Th8;
then u1,v1,u,v are_Ort_wrt w,y by Def3;
hence p1,q1 _|_ p,q by Th31; :: thesis: verum