for V being RealLinearSpace
for u, u1, v, 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 by ANALOAF:12, Lm4;