let V be RealLinearSpace; :: thesis: for w, y, u, v being VECTOR of V st Gen w,y holds
u,u,v,v are_DTr_wrt w,y
let w, y, u, v be VECTOR of V; :: thesis: ( Gen w,y implies u,u,v,v are_DTr_wrt w,y )
assume Gen w,y ; :: thesis: u,u,v,v are_DTr_wrt w,y
then A1: ( u,u,u # u,v # v are_Ort_wrt w,y & v,v,u # u,v # v are_Ort_wrt w,y ) by Lm5, Lm6;
u,u // v,v by ANALOAF:9;
hence u,u,v,v are_DTr_wrt w,y by A1, Def3; :: thesis: verum