let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y being VECTOR of V st u,v,u1,v1 are_DTr_wrt w,y holds
v,u,v1,u1 are_DTr_wrt w,y
let u, u1, v, v1, w, y be VECTOR of V; :: thesis: ( u,v,u1,v1 are_DTr_wrt w,y implies v,u,v1,u1 are_DTr_wrt w,y )
assume A1: u,v,u1,v1 are_DTr_wrt w,y ; :: thesis: v,u,v1,u1 are_DTr_wrt w,y
then u,v // u1,v1 ;
then A2: v,u // v1,u1 by ANALOAF:12;

A3: now :: thesis: for u, u9, v, v9 being VECTOR of V st u,u9,v,v9 are_Ort_wrt w,y holds
u9,u,v,v9 are_Ort_wrt w,y

let u, u9, v, v9 be VECTOR of V; :: thesis: ( u,u9,v,v9 are_Ort_wrt w,y implies u9,u,v,v9 are_Ort_wrt w,y )
assume u,u9,v,v9 are_Ort_wrt w,y ; :: thesis: u9,u,v,v9 are_Ort_wrt w,y
then v,v9,u,u9 are_Ort_wrt w,y by Lm5;
then v,v9,u9,u are_Ort_wrt w,y by Lm4;
hence u9,u,v,v9 are_Ort_wrt w,y by Lm5; :: thesis: verum

end;

u1,v1,u # v,u1 # v1 are_Ort_wrt w,y by A1;
then A4: v1,u1,v # u,v1 # u1 are_Ort_wrt w,y by A3;
u,v,u # v,u1 # v1 are_Ort_wrt w,y by A1;
then v,u,v # u,v1 # u1 are_Ort_wrt w,y by A3;
hence v,u,v1,u1 are_DTr_wrt w,y by A2, A4; :: thesis: verum