theorem Th12: :: ANALMETR:12

for V being RealLinearSpace
for u, u1, u2, w, y being VECTOR of V st Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y holds
u2,u - u1 are_Ort_wrt w,y