let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st u,v are_Ort_wrt w,y holds
v,u are_Ort_wrt w,y
let u, v, w, y be VECTOR of V; :: thesis: ( u,v are_Ort_wrt w,y implies v,u are_Ort_wrt w,y )
assume u,v are_Ort_wrt w,y ; :: thesis: v,u are_Ort_wrt w,y
then consider a1, a2, b1, b2 being Real such that
A1: ( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) ) and
A2: (a1 * b1) + (a2 * b2) = 0 by Def2;
thus v,u are_Ort_wrt w,y by A1, A2, Def2; :: thesis: verum