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