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