let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y being VECTOR of V st u,v,u1,v1 are_Ort_wrt w,y holds
u1,v1,u,v are_Ort_wrt w,y
let u, u1, v, v1, w, y be VECTOR of V; :: thesis: ( u,v,u1,v1 are_Ort_wrt w,y implies u1,v1,u,v are_Ort_wrt w,y )
assume u,v,u1,v1 are_Ort_wrt w,y ; :: thesis: u1,v1,u,v are_Ort_wrt w,y
then v - u,v1 - u1 are_Ort_wrt w,y by ANALMETR:def 3;
then v1 - u1,v - u are_Ort_wrt w,y by ANALMETR:4;
hence u1,v1,u,v are_Ort_wrt w,y by ANALMETR:def 3; :: thesis: verum